Add Armv8.1-M Keccak x1 backend by bremoran · Pull Request #1277 · pq-code-package/mldsa-native

bremoran · 2026-07-10T08:11:34Z

Add the unmodified upstream Adomnicai Armv7-M Keccak source under armv81m_clean and the Slothy-generated M7 optimized x1 permutation under armv81m_opt, with a Makefile regeneration path.

Move the Armv8.1-M FIPS202 development sources to armv81m_opt and synchronize the production backend. Route x1 state XOR/extract through the clean-source assembly helpers so the optimized permutation can keep the state in the bit-interleaved native representation.

Keep the test changes focused on representation-aware Keccak x1/x4 unit coverage, including extracted-byte state dumps on x1 failures, and the static ML-DSA-87 unit-test workspace needed for Zephyr stack pressure.

Fixes #1322

oqs-bot · 2026-07-10T16:09:56Z

CBMC Results (ML-DSA-44)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`compute_pack_t0_t1`	⚠️	100s	50s	+100%
`mld_attempt_signature_generation`	⚠️	295s	58s	+409%
`sig_unpack_hints`	⚠️	21s	2s	+950%
`sign_keypair_internal`	⚠️	22s	4s	+450%
`sign_pk_from_sk`	⚠️	35s	5s	+600%
`sign_signature_internal`	⚠️	97s	26s	+273%
`sign_verify_internal`	⚠️	290s	114s	+154%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1863s	1514s	+23.1%
`mld_attempt_signature_generation`	⚠️	295s	58s	+409%
`sign_verify_internal`	⚠️	290s	114s	+154%
`polyvecl_pointwise_acc_montgomery_c`	✅	151s	131s	+15%
`poly_pointwise_montgomery_c`	✅	146s	114s	+28%
`compute_pack_t0_t1`	⚠️	100s	50s	+100%
`sign_signature_internal`	⚠️	97s	26s	+273%
`mld_invntt_layer`	✅	58s	107s	-46%
`sign_pk_from_sk`	⚠️	35s	5s	+600%
`fqmul`	✅	25s	39s	-36%
`sign_keypair_internal`	⚠️	22s	4s	+450%
`mld_ntt_layer`	✅	21s	42s	-50%
`sig_unpack_hints`	⚠️	21s	2s	+950%
`polyvec_matrix_expand`	✅	17s	28s	-39%
`keccakf1600x4_permute_native`	✅	12s	22s	-45%
`mld_ntt_butterfly_block`	✅	12s	23s	-48%
`polyt0_unpack`	✅	11s	15s	-27%
`poly_ntt_c`	✅	10s	19s	-47%
`rej_uniform`	✅	10s	18s	-44%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	9s	15s	-40%
`rej_uniform_native_x86_64`	✅	9s	-	new
`mld_check_pct`	✅	8s	14s	-43%
`poly_uniform_eta_4x`	✅	8s	11s	-27%
`polyeta_unpack`	✅	8s	14s	-43%
`mld_compute_pack_z`	✅	7s	7s	+0%
`poly_invntt_tomont_c`	✅	7s	11s	-36%
`poly_uniform_4x`	✅	7s	14s	-50%
`rej_uniform_c`	✅	7s	15s	-53%
`keccak_absorb_once_x4`	✅	6s	9s	-33%
`keccakf1600_xor_bytes`	✅	6s	1s	+500%
`mld_sample_s1_s2`	✅	6s	4s	+50%
`montgomery_reduce`	✅	6s	3s	+100%
`pointwise_acc_native_aarch64`	✅	6s	4s	+50%
`polyz_unpack_c`	✅	6s	11s	-45%
`sign_keypair`	✅	6s	4s	+50%
`mld_h`	✅	5s	4s	+25%
`poly_chknorm_c`	✅	5s	17s	-71%
`poly_use_hint_native_aarch64`	✅	5s	2s	+150%
`keccak_squeezeblocks_x4`	✅	4s	4s	+0%
`keccakf1600x4_extract_bytes`	✅	4s	2s	+100%
`mld_ct_cmask_nonzero_u32`	✅	4s	2s	+100%
`mld_keccakf1600_permute_c`	✅	4s	8s	-50%
`pointwise_acc_native_x86_64`	✅	4s	7s	-43%
`poly_add`	✅	4s	7s	-43%
`poly_caddq_native_aarch64`	✅	4s	4s	+0%
`poly_chknorm_native_aarch64`	✅	4s	4s	+0%
`poly_decompose_88_native_aarch64`	✅	4s	4s	+0%
`poly_permute_bitrev_to_custom_optional_native`	✅	4s	4s	+0%
`poly_power2round`	✅	4s	4s	+0%
`polyveck_decompose`	✅	4s	4s	+0%
`polyvecl_chknorm`	✅	4s	10s	-60%
`polyvecl_pack_eta`	✅	4s	3s	+33%
`polyz_unpack`	✅	4s	3s	+33%
`rej_uniform_native`	✅	4s	4s	+0%
`sign_signature_extmu`	✅	4s	4s	+0%
`sign_signature_pre_hash_internal`	✅	4s	6s	-33%
`sign_signature_pre_hash_shake256`	✅	4s	3s	+33%
`sk_s2hat_get_poly`	✅	4s	2s	+100%
`unpack_sk`	✅	4s	3s	+33%
`decompose`	✅	3s	2s	+50%
`intt_native_aarch64`	✅	3s	9s	-67%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	3s	3s	+0%
`keccakf1600_permute_native`	✅	3s	3s	+0%
`keccakf1600x4_extract_bytes_native`	✅	3s	3s	+0%
`mld_ct_abs_i32`	✅	3s	2s	+50%
`mld_ct_cmask_neg_i32`	✅	3s	3s	+0%
`mld_ct_get_optblocker_u32`	✅	3s	1s	+200%
`mld_keccakf1600x4_extract_bytes_c`	✅	3s	2s	+50%
`mld_polymat_expand_entry`	✅	3s	3s	+0%
`mld_sign_attempt`	✅	3s	-	new
`mld_sign_resume`	✅	3s	-	new
`mld_value_barrier_u32`	✅	3s	2s	+50%
`ntt_native_aarch64`	✅	3s	3s	+0%
`pack_sig_c`	✅	3s	2s	+50%
`pack_sk_s1`	✅	3s	2s	+50%
`pointwise_native_aarch64`	✅	3s	5s	-40%
`pointwise_native_x86_64`	✅	3s	4s	-25%
`poly_challenge`	✅	3s	3s	+0%
`poly_chknorm`	✅	3s	4s	-25%
`poly_chknorm_native_x86_64`	✅	3s	2s	+50%
`poly_decompose_32_native_aarch64`	✅	3s	2s	+50%
`poly_decompose_c`	✅	3s	4s	-25%
`poly_invntt_tomont`	✅	3s	4s	-25%
`poly_ntt_native`	✅	3s	5s	-40%
`poly_permute_bitrev_to_custom_optional`	✅	3s	2s	+50%
`poly_pointwise_montgomery_native`	✅	3s	2s	+50%
`poly_use_hint_native`	✅	3s	4s	-25%
`polyeta_pack`	✅	3s	3s	+0%
`polyt0_pack`	✅	3s	2s	+50%
`polyt1_unpack`	✅	3s	5s	-40%
`polyvec_matrix_pointwise_montgomery_row`	✅	3s	2s	+50%
`polyveck_caddq`	✅	3s	3s	+0%
`polyveck_chknorm`	✅	3s	5s	-40%
`polyveck_pack_w1`	✅	3s	1s	+200%
`polyveck_reduce`	✅	3s	5s	-40%
`polyvecl_ntt`	✅	3s	2s	+50%
`polyvecl_uniform_gamma1`	✅	3s	3s	+0%
`polyvecl_unpack_z`	✅	3s	2s	+50%
`polyw1_pack_32`	✅	3s	2s	+50%
`rej_eta`	✅	3s	3s	+0%
`shake128_squeeze`	✅	3s	1s	+200%
`shake256x4_squeezeblocks`	✅	3s	4s	-25%
`sign_verify_extmu`	✅	3s	3s	+0%
`sign_verify_pre_hash_shake256`	✅	3s	5s	-40%
`sk_t0hat_get_poly`	✅	3s	2s	+50%
`unpack_pk_t1`	✅	3s	5s	-40%
`unpack_sk_s2hat`	✅	3s	4s	-25%
`unpack_sk_t0hat`	✅	3s	3s	+0%
`yvec_get_poly`	✅	3s	3s	+0%
`yvec_init`	✅	3s	3s	+0%
`fqscale`	✅	2s	3s	-33%
`keccak_absorb`	✅	2s	5s	-60%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	1s	+100%
`keccak_finalize`	✅	2s	3s	-33%
`keccak_init`	✅	2s	3s	-33%
`keccak_squeeze`	✅	2s	1s	+100%
`keccakf1600_extract_bytes (big endian)`	✅	2s	2s	+0%
`keccakf1600x4_permute`	✅	2s	4s	-50%
`keccakf1600x4_xor_bytes`	✅	2s	2s	+0%
`mld_ct_memcmp`	✅	2s	3s	-33%
`mld_keccakf1600_extract_bytes`	✅	2s	2s	+0%
`mld_prepare_domain_separation_prefix`	✅	2s	4s	-50%
`mld_sample_s1_s2_serial`	✅	2s	3s	-33%
`mld_value_barrier_i64`	✅	2s	2s	+0%
`mld_value_barrier_u8`	✅	2s	3s	-33%
`ntt_native_x86_64`	✅	2s	3s	-33%
`pack_sig_h`	✅	2s	3s	-33%
`pack_sig_z`	✅	2s	4s	-50%
`pack_sk_rho_key_tr_s2`	✅	2s	3s	-33%
`poly_caddq`	✅	2s	2s	+0%
`poly_caddq_native`	✅	2s	5s	-60%
`poly_caddq_native_x86_64`	✅	2s	4s	-50%
`poly_chknorm_native`	✅	2s	4s	-50%
`poly_decompose`	✅	2s	3s	-33%
`poly_decompose_native`	✅	2s	3s	-33%
`poly_decompose_native_x86_64`	✅	2s	3s	-33%
`poly_invntt_tomont_native`	✅	2s	4s	-50%
`poly_pointwise_montgomery`	✅	2s	3s	-33%
`poly_reduce`	✅	2s	3s	-33%
`poly_shiftl`	✅	2s	3s	-33%
`poly_sub`	✅	2s	3s	-33%
`poly_uniform`	✅	2s	6s	-67%
`poly_uniform_eta`	✅	2s	5s	-60%
`poly_uniform_gamma1`	✅	2s	4s	-50%
`poly_uniform_gamma1_4x`	✅	2s	5s	-60%
`poly_use_hint`	✅	2s	4s	-50%
`poly_use_hint_c`	✅	2s	3s	-33%
`polyveck_invntt_tomont`	✅	2s	5s	-60%
`polyveck_ntt`	✅	2s	5s	-60%
`polyveck_pack_eta`	✅	2s	2s	+0%
`polyveck_unpack_eta`	✅	2s	2s	+0%
`polyvecl_pointwise_acc_montgomery`	✅	2s	4s	-50%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	2s	+0%
`polyvecl_unpack_eta`	✅	2s	2s	+0%
`polyw1_pack`	✅	2s	3s	-33%
`polyz_unpack_19_native_aarch64`	✅	2s	5s	-60%
`polyz_unpack_native`	✅	2s	2s	+0%
`polyz_unpack_native_x86_64`	✅	2s	3s	-33%
`rej_uniform_eta_native_aarch64`	✅	2s	2s	+0%
`rej_uniform_eta_native_x86_64`	✅	2s	-	new
`rej_uniform_native_aarch64`	✅	2s	5s	-60%
`shake128_absorb`	✅	2s	2s	+0%
`shake128_finalize`	✅	2s	2s	+0%
`shake128_init`	✅	2s	3s	-33%
`shake128x4_squeezeblocks`	✅	2s	1s	+100%
`shake256_init`	✅	2s	3s	-33%
`shake256x4_absorb_once`	✅	2s	3s	-33%
`sign_signature`	✅	2s	3s	-33%
`sign_verify`	✅	2s	4s	-50%
`sign_verify_pre_hash_internal`	✅	2s	3s	-33%
`sk_s1hat_get_poly`	✅	2s	3s	-33%
`sys_check_capability`	✅	2s	4s	-50%
`unpack_sk_s1hat`	✅	2s	1s	+100%
`use_hint`	✅	2s	2s	+0%
`caddq`	✅	1s	2s	-50%
`intt_native_x86_64`	✅	1s	4s	-75%
`keccak_f1600_x1_native_aarch64`	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v84a`	✅	1s	2s	-50%
`keccak_f1600_x4_native_avx2`	✅	1s	3s	-67%
`keccakf1600_permute`	✅	1s	2s	-50%
`keccakf1600_xor_bytes (big endian)`	✅	1s	4s	-75%
`keccakf1600x4_xor_bytes_native`	✅	1s	3s	-67%
`make_hint`	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u8`	✅	1s	2s	-50%
`mld_ct_get_optblocker_i64`	✅	1s	4s	-75%
`mld_ct_get_optblocker_u8`	✅	1s	1s	+0%
`mld_ct_sel_int32`	✅	1s	2s	-50%
`mld_keccakf1600x4_xor_bytes_c`	✅	1s	2s	-50%
`mld_sign_finish`	✅	1s	-	new
`nttunpack_native_x86_64`	✅	1s	1s	+0%
`poly_caddq_c`	✅	1s	2s	-50%
`poly_ntt`	✅	1s	3s	-67%
`poly_use_hint_native_x86_64`	✅	1s	-	new
`polyt1_pack`	✅	1s	4s	-75%
`polyvec_matrix_expand_serial`	✅	1s	8s	-88%
`polyvecl_uniform_gamma1_serial`	✅	1s	2s	-50%
`polyw1_pack_88`	✅	1s	1s	+0%
`polyz_pack`	✅	1s	2s	-50%
`polyz_unpack_17_native_aarch64`	✅	1s	5s	-80%
`power2round`	✅	1s	3s	-67%
`reduce32`	✅	1s	2s	-50%
`rej_eta_c`	✅	1s	4s	-75%
`rej_eta_native`	✅	1s	6s	-83%
`shake128_release`	✅	1s	1s	+0%
`shake128x4_absorb_once`	✅	1s	3s	-67%
`shake256`	✅	1s	1s	+0%
`shake256_absorb`	✅	1s	3s	-67%
`shake256_finalize`	✅	1s	2s	-50%
`shake256_release`	✅	1s	2s	-50%
`shake256_squeeze`	✅	1s	2s	-50%

oqs-bot · 2026-07-10T16:10:06Z

CBMC Results (ML-DSA-44, REDUCE-RAM)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`compute_pack_t0_t1`	⚠️	29s	12s	+142%
`mld_attempt_signature_generation`	⚠️	143s	19s	+653%
`sign_keypair_internal`	⚠️	20s	4s	+400%
`sign_pk_from_sk`	⚠️	38s	5s	+660%
`sign_verify_internal`	⚠️	156s	49s	+218%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1225s	1364s	-10.2%
`sign_verify_internal`	⚠️	156s	49s	+218%
`mld_attempt_signature_generation`	⚠️	143s	19s	+653%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	100s	149s	-33%
`poly_pointwise_montgomery_c`	✅	63s	112s	-44%
`mld_invntt_layer`	✅	56s	105s	-47%
`sign_pk_from_sk`	⚠️	38s	5s	+660%
`compute_pack_t0_t1`	⚠️	29s	12s	+142%
`fqmul`	✅	23s	39s	-41%
`mld_ntt_layer`	✅	22s	41s	-46%
`sign_keypair_internal`	⚠️	20s	4s	+400%
`keccakf1600x4_permute_native`	✅	12s	22s	-45%
`rej_uniform_c`	✅	12s	16s	-25%
`sign_signature_internal`	✅	12s	4s	+200%
`mld_ntt_butterfly_block`	✅	11s	23s	-52%
`sig_unpack_hints`	✅	11s	2s	+450%
`poly_ntt_c`	✅	9s	21s	-57%
`rej_uniform`	✅	9s	8s	+12%
`poly_invntt_tomont_c`	✅	8s	11s	-27%
`polyeta_unpack`	✅	8s	14s	-43%
`polyt0_unpack`	✅	8s	12s	-33%
`poly_uniform_eta_4x`	✅	7s	12s	-42%
`polyz_unpack_c`	✅	7s	8s	-12%
`rej_uniform_native_x86_64`	✅	7s	-	new
`polyveck_decompose`	✅	6s	7s	-14%
`sign_keypair`	✅	6s	5s	+20%
`keccak_absorb_once_x4`	✅	5s	8s	-38%
`pointwise_acc_native_x86_64`	✅	5s	4s	+25%
`poly_power2round`	✅	5s	4s	+25%
`polyvec_matrix_pointwise_montgomery_row`	✅	5s	6s	-17%
`polyveck_pack_eta`	✅	5s	4s	+25%
`rej_uniform_native`	✅	5s	5s	+0%
`sign_signature`	✅	5s	6s	-17%
`sk_s2hat_get_poly`	✅	5s	5s	+0%
`keccak_absorb`	✅	4s	3s	+33%
`keccak_f1600_x4_native_aarch64_v84a`	✅	4s	3s	+33%
`keccak_squeezeblocks_x4`	✅	4s	3s	+33%
`mld_check_pct`	✅	4s	15s	-73%
`mld_sign_finish`	✅	4s	-	new
`pack_sk_s1`	✅	4s	3s	+33%
`poly_add`	✅	4s	7s	-43%
`poly_chknorm_c`	✅	4s	11s	-64%
`poly_invntt_tomont_native`	✅	4s	3s	+33%
`polyt1_unpack`	✅	4s	2s	+100%
`polyvec_matrix_expand_serial`	✅	4s	4s	+0%
`polyvecl_chknorm`	✅	4s	11s	-64%
`polyvecl_pack_eta`	✅	4s	2s	+100%
`polyz_unpack_native_x86_64`	✅	4s	3s	+33%
`rej_eta_native`	✅	4s	3s	+33%
`rej_uniform_eta_native_aarch64`	✅	4s	3s	+33%
`shake128_squeeze`	✅	4s	2s	+100%
`sign_signature_pre_hash_internal`	✅	4s	4s	+0%
`sign_signature_pre_hash_shake256`	✅	4s	4s	+0%
`caddq`	✅	3s	6s	-50%
`decompose`	✅	3s	3s	+0%
`intt_native_x86_64`	✅	3s	2s	+50%
`keccak_f1600_x1_native_aarch64`	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	3s	2s	+50%
`keccak_init`	✅	3s	3s	+0%
`keccak_squeeze`	✅	3s	2s	+50%
`keccakf1600_extract_bytes (big endian)`	✅	3s	4s	-25%
`keccakf1600x4_extract_bytes_native`	✅	3s	4s	-25%
`make_hint`	✅	3s	3s	+0%
`mld_compute_pack_z`	✅	3s	6s	-50%
`mld_ct_cmask_nonzero_u32`	✅	3s	3s	+0%
`mld_ct_cmask_nonzero_u8`	✅	3s	2s	+50%
`mld_keccakf1600_permute_c`	✅	3s	7s	-57%
`mld_keccakf1600x4_xor_bytes_c`	✅	3s	4s	-25%
`mld_sample_s1_s2`	✅	3s	1s	+200%
`mld_sign_attempt`	✅	3s	-	new
`montgomery_reduce`	✅	3s	2s	+50%
`ntt_native_aarch64`	✅	3s	4s	-25%
`ntt_native_x86_64`	✅	3s	3s	+0%
`pointwise_native_aarch64`	✅	3s	2s	+50%
`poly_caddq`	✅	3s	4s	-25%
`poly_challenge`	✅	3s	6s	-50%
`poly_chknorm`	✅	3s	3s	+0%
`poly_chknorm_native`	✅	3s	4s	-25%
`poly_chknorm_native_x86_64`	✅	3s	2s	+50%
`poly_decompose`	✅	3s	2s	+50%
`poly_decompose_c`	✅	3s	5s	-40%
`poly_decompose_native`	✅	3s	2s	+50%
`poly_decompose_native_x86_64`	✅	3s	2s	+50%
`poly_permute_bitrev_to_custom_optional_native`	✅	3s	3s	+0%
`poly_shiftl`	✅	3s	4s	-25%
`poly_use_hint_c`	✅	3s	5s	-40%
`poly_use_hint_native`	✅	3s	3s	+0%
`poly_use_hint_native_x86_64`	✅	3s	-	new
`polyveck_caddq`	✅	3s	3s	+0%
`polyveck_invntt_tomont`	✅	3s	5s	-40%
`polyveck_reduce`	✅	3s	4s	-25%
`polyvecl_unpack_eta`	✅	3s	4s	-25%
`polyvecl_unpack_z`	✅	3s	3s	+0%
`polyz_pack`	✅	3s	2s	+50%
`polyz_unpack`	✅	3s	3s	+0%
`polyz_unpack_19_native_aarch64`	✅	3s	4s	-25%
`polyz_unpack_native`	✅	3s	3s	+0%
`reduce32`	✅	3s	3s	+0%
`rej_eta`	✅	3s	5s	-40%
`rej_uniform_eta_native_x86_64`	✅	3s	-	new
`shake128x4_squeezeblocks`	✅	3s	2s	+50%
`shake256`	✅	3s	1s	+200%
`shake256_finalize`	✅	3s	2s	+50%
`shake256_init`	✅	3s	4s	-25%
`sign_signature_extmu`	✅	3s	4s	-25%
`sign_verify`	✅	3s	4s	-25%
`sign_verify_extmu`	✅	3s	5s	-40%
`sign_verify_pre_hash_shake256`	✅	3s	5s	-40%
`sk_t0hat_get_poly`	✅	3s	1s	+200%
`unpack_sk`	✅	3s	3s	+0%
`use_hint`	✅	3s	2s	+50%
`yvec_init`	✅	3s	1s	+200%
`intt_native_aarch64`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	2s	+0%
`keccak_f1600_x4_native_avx2`	✅	2s	2s	+0%
`keccakf1600_permute`	✅	2s	2s	+0%
`keccakf1600_xor_bytes (big endian)`	✅	2s	6s	-67%
`keccakf1600x4_extract_bytes`	✅	2s	2s	+0%
`keccakf1600x4_permute`	✅	2s	4s	-50%
`keccakf1600x4_xor_bytes_native`	✅	2s	5s	-60%
`mld_ct_memcmp`	✅	2s	1s	+100%
`mld_ct_sel_int32`	✅	2s	3s	-33%
`mld_h`	✅	2s	4s	-50%
`mld_keccakf1600x4_extract_bytes_c`	✅	2s	4s	-50%
`mld_value_barrier_i64`	✅	2s	3s	-33%
`mld_value_barrier_u8`	✅	2s	4s	-50%
`nttunpack_native_x86_64`	✅	2s	4s	-50%
`pack_sig_c`	✅	2s	5s	-60%
`pack_sig_h`	✅	2s	4s	-50%
`pack_sk_rho_key_tr_s2`	✅	2s	5s	-60%
`pointwise_acc_native_aarch64`	✅	2s	6s	-67%
`poly_caddq_native`	✅	2s	3s	-33%
`poly_caddq_native_aarch64`	✅	2s	3s	-33%
`poly_caddq_native_x86_64`	✅	2s	4s	-50%
`poly_chknorm_native_aarch64`	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	✅	2s	4s	-50%
`poly_decompose_88_native_aarch64`	✅	2s	3s	-33%
`poly_invntt_tomont`	✅	2s	2s	+0%
`poly_ntt_native`	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional`	✅	2s	5s	-60%
`poly_reduce`	✅	2s	4s	-50%
`poly_uniform`	✅	2s	3s	-33%
`poly_uniform_eta`	✅	2s	2s	+0%
`poly_use_hint_native_aarch64`	✅	2s	3s	-33%
`polyeta_pack`	✅	2s	3s	-33%
`polyt0_pack`	✅	2s	4s	-50%
`polyvec_matrix_expand`	✅	2s	3s	-33%
`polyveck_pack_w1`	✅	2s	3s	-33%
`polyveck_unpack_eta`	✅	2s	2s	+0%
`polyvecl_ntt`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	3s	-33%
`polyw1_pack`	✅	2s	4s	-50%
`polyw1_pack_88`	✅	2s	2s	+0%
`polyz_unpack_17_native_aarch64`	✅	2s	2s	+0%
`rej_uniform_native_aarch64`	✅	2s	3s	-33%
`shake128_finalize`	✅	2s	3s	-33%
`shake256_release`	✅	2s	1s	+100%
`shake256x4_absorb_once`	✅	2s	1s	+100%
`sign_verify_pre_hash_internal`	✅	2s	5s	-60%
`sk_s1hat_get_poly`	✅	2s	2s	+0%
`sys_check_capability`	✅	2s	2s	+0%
`unpack_sk_t0hat`	✅	2s	2s	+0%
`fqscale`	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	1s	3s	-67%
`keccak_finalize`	✅	1s	2s	-50%
`keccakf1600_permute_native`	✅	1s	3s	-67%
`keccakf1600_xor_bytes`	✅	1s	3s	-67%
`keccakf1600x4_xor_bytes`	✅	1s	3s	-67%
`mld_ct_abs_i32`	✅	1s	3s	-67%
`mld_ct_cmask_neg_i32`	✅	1s	2s	-50%
`mld_ct_get_optblocker_i64`	✅	1s	4s	-75%
`mld_ct_get_optblocker_u32`	✅	1s	2s	-50%
`mld_ct_get_optblocker_u8`	✅	1s	2s	-50%
`mld_keccakf1600_extract_bytes`	✅	1s	2s	-50%
`mld_polymat_expand_entry`	✅	1s	2s	-50%
`mld_prepare_domain_separation_prefix`	✅	1s	3s	-67%
`mld_sample_s1_s2_serial`	✅	1s	4s	-75%
`mld_sign_resume`	✅	1s	-	new
`mld_value_barrier_u32`	✅	1s	1s	+0%
`pack_sig_z`	✅	1s	2s	-50%
`pointwise_native_x86_64`	✅	1s	4s	-75%
`poly_caddq_c`	✅	1s	3s	-67%
`poly_ntt`	✅	1s	3s	-67%
`poly_pointwise_montgomery`	✅	1s	3s	-67%
`poly_pointwise_montgomery_native`	✅	1s	2s	-50%
`poly_sub`	✅	1s	3s	-67%
`poly_uniform_4x`	✅	1s	3s	-67%
`poly_uniform_gamma1`	✅	1s	3s	-67%
`poly_uniform_gamma1_4x`	✅	1s	5s	-80%
`poly_use_hint`	✅	1s	2s	-50%
`polyt1_pack`	✅	1s	3s	-67%
`polyveck_chknorm`	✅	1s	67s	-99%
`polyveck_ntt`	✅	1s	2s	-50%
`polyvecl_pointwise_acc_montgomery`	✅	1s	3s	-67%
`polyvecl_pointwise_acc_montgomery_c`	✅	1s	4s	-75%
`polyvecl_uniform_gamma1`	✅	1s	2s	-50%
`polyvecl_uniform_gamma1_serial`	✅	1s	2s	-50%
`polyw1_pack_32`	✅	1s	3s	-67%
`power2round`	✅	1s	2s	-50%
`rej_eta_c`	✅	1s	4s	-75%
`shake128_absorb`	✅	1s	3s	-67%
`shake128_init`	✅	1s	2s	-50%
`shake128_release`	✅	1s	2s	-50%
`shake128x4_absorb_once`	✅	1s	2s	-50%
`shake256_absorb`	✅	1s	2s	-50%
`shake256_squeeze`	✅	1s	2s	-50%
`shake256x4_squeezeblocks`	✅	1s	2s	-50%
`unpack_pk_t1`	✅	1s	3s	-67%
`unpack_sk_s1hat`	✅	1s	3s	-67%
`unpack_sk_s2hat`	✅	1s	4s	-75%
`yvec_get_poly`	✅	1s	3s	-67%

oqs-bot · 2026-07-10T16:10:13Z

CBMC Results (ML-DSA-87, REDUCE-RAM)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`compute_pack_t0_t1`	⚠️	28s	12s	+133%
`mld_attempt_signature_generation`	⚠️	243s	34s	+615%
`sign_keypair_internal`	⚠️	46s	6s	+667%
`sign_pk_from_sk`	⚠️	61s	6s	+917%
`sign_verify_internal`	⚠️	314s	47s	+568%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1655s	1436s	+15.3%
`sign_verify_internal`	⚠️	314s	47s	+568%
`mld_attempt_signature_generation`	⚠️	243s	34s	+615%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	198s	196s	+1%
`poly_pointwise_montgomery_c`	✅	66s	125s	-47%
`sign_pk_from_sk`	⚠️	61s	6s	+917%
`mld_invntt_layer`	✅	58s	111s	-48%
`sign_keypair_internal`	⚠️	46s	6s	+667%
`compute_pack_t0_t1`	⚠️	28s	12s	+133%
`fqmul`	✅	24s	39s	-38%
`mld_ntt_layer`	✅	22s	44s	-50%
`sign_signature_internal`	✅	13s	3s	+333%
`rej_uniform_c`	✅	12s	18s	-33%
`keccakf1600x4_permute_native`	✅	11s	25s	-56%
`mld_ntt_butterfly_block`	✅	11s	23s	-52%
`sig_unpack_hints`	✅	11s	4s	+175%
`poly_ntt_c`	✅	10s	19s	-47%
`rej_uniform`	✅	10s	7s	+43%
`polyt0_unpack`	✅	8s	14s	-43%
`polyveck_decompose`	✅	8s	12s	-33%
`polyvecl_ntt`	✅	8s	8s	+0%
`polyeta_unpack`	✅	7s	13s	-46%
`poly_invntt_tomont_c`	✅	6s	9s	-33%
`poly_invntt_tomont_native`	✅	6s	2s	+200%
`poly_uniform_eta_4x`	✅	6s	12s	-50%
`rej_uniform_native_x86_64`	✅	6s	-	new
`sign_signature`	✅	6s	4s	+50%
`sk_t0hat_get_poly`	✅	6s	3s	+100%
`keccak_absorb_once_x4`	✅	5s	8s	-38%
`mld_check_pct`	✅	5s	15s	-67%
`pointwise_acc_native_x86_64`	✅	5s	8s	-38%
`poly_chknorm_c`	✅	5s	13s	-62%
`polyvec_matrix_pointwise_montgomery_row`	✅	5s	13s	-62%
`polyveck_ntt`	✅	5s	3s	+67%
`polyvecl_chknorm`	✅	5s	38s	-87%
`polyw1_pack_32`	✅	5s	3s	+67%
`sign_keypair`	✅	5s	4s	+25%
`sign_signature_extmu`	✅	5s	4s	+25%
`sign_signature_pre_hash_shake256`	✅	5s	3s	+67%
`sk_s1hat_get_poly`	✅	5s	3s	+67%
`keccak_absorb`	✅	4s	4s	+0%
`keccak_finalize`	✅	4s	1s	+300%
`keccakf1600_permute`	✅	4s	2s	+100%
`mld_sample_s1_s2_serial`	✅	4s	6s	-33%
`mld_sign_finish`	✅	4s	-	new
`ntt_native_x86_64`	✅	4s	2s	+100%
`pointwise_acc_native_aarch64`	✅	4s	5s	-20%
`poly_caddq_native_aarch64`	✅	4s	3s	+33%
`poly_chknorm`	✅	4s	4s	+0%
`poly_power2round`	✅	4s	7s	-43%
`poly_uniform_gamma1`	✅	4s	3s	+33%
`polyveck_invntt_tomont`	✅	4s	4s	+0%
`polyveck_reduce`	✅	4s	6s	-33%
`polyz_pack`	✅	4s	4s	+0%
`rej_eta_native`	✅	4s	4s	+0%
`shake128x4_squeezeblocks`	✅	4s	1s	+300%
`yvec_get_poly`	✅	4s	2s	+100%
`caddq`	✅	3s	3s	+0%
`intt_native_aarch64`	✅	3s	4s	-25%
`keccak_f1600_x1_native_aarch64_v84a`	✅	3s	2s	+50%
`keccak_init`	✅	3s	1s	+200%
`keccakf1600_xor_bytes (big endian)`	✅	3s	2s	+50%
`keccakf1600x4_extract_bytes`	✅	3s	1s	+200%
`keccakf1600x4_extract_bytes_native`	✅	3s	4s	-25%
`mld_compute_pack_z`	✅	3s	6s	-50%
`mld_ct_cmask_nonzero_u32`	✅	3s	5s	-40%
`mld_ct_get_optblocker_i64`	✅	3s	2s	+50%
`mld_ct_get_optblocker_u32`	✅	3s	2s	+50%
`mld_ct_sel_int32`	✅	3s	2s	+50%
`mld_keccakf1600_permute_c`	✅	3s	8s	-62%
`mld_keccakf1600x4_extract_bytes_c`	✅	3s	3s	+0%
`mld_sample_s1_s2`	✅	3s	8s	-62%
`mld_sign_attempt`	✅	3s	-	new
`mld_sign_resume`	✅	3s	-	new
`mld_value_barrier_u32`	✅	3s	3s	+0%
`montgomery_reduce`	✅	3s	2s	+50%
`pack_sig_h`	✅	3s	3s	+0%
`pack_sk_rho_key_tr_s2`	✅	3s	2s	+50%
`poly_add`	✅	3s	8s	-62%
`poly_caddq_native_x86_64`	✅	3s	3s	+0%
`poly_chknorm_native`	✅	3s	1s	+200%
`poly_chknorm_native_aarch64`	✅	3s	5s	-40%
`poly_chknorm_native_x86_64`	✅	3s	2s	+50%
`poly_ntt`	✅	3s	2s	+50%
`poly_ntt_native`	✅	3s	4s	-25%
`poly_permute_bitrev_to_custom_optional_native`	✅	3s	3s	+0%
`poly_use_hint_native`	✅	3s	1s	+200%
`polyeta_pack`	✅	3s	3s	+0%
`polyt0_pack`	✅	3s	3s	+0%
`polyt1_pack`	✅	3s	5s	-40%
`polyt1_unpack`	✅	3s	3s	+0%
`polyvec_matrix_expand_serial`	✅	3s	3s	+0%
`polyveck_pack_eta`	✅	3s	5s	-40%
`polyvecl_pack_eta`	✅	3s	2s	+50%
`polyvecl_pointwise_acc_montgomery`	✅	3s	2s	+50%
`polyvecl_uniform_gamma1`	✅	3s	3s	+0%
`polyvecl_unpack_eta`	✅	3s	3s	+0%
`polyz_unpack_19_native_aarch64`	✅	3s	5s	-40%
`polyz_unpack_native_x86_64`	✅	3s	3s	+0%
`power2round`	✅	3s	3s	+0%
`rej_eta`	✅	3s	2s	+50%
`rej_uniform_eta_native_aarch64`	✅	3s	3s	+0%
`shake128_absorb`	✅	3s	2s	+50%
`shake128_release`	✅	3s	3s	+0%
`shake128_squeeze`	✅	3s	1s	+200%
`sign_signature_pre_hash_internal`	✅	3s	2s	+50%
`unpack_sk`	✅	3s	4s	-25%
`unpack_sk_s2hat`	✅	3s	3s	+0%
`unpack_sk_t0hat`	✅	3s	4s	-25%
`decompose`	✅	2s	2s	+0%
`intt_native_x86_64`	✅	2s	4s	-50%
`keccak_f1600_x4_native_aarch64_v84a`	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	2s	+0%
`keccak_squeeze`	✅	2s	5s	-60%
`keccak_squeezeblocks_x4`	✅	2s	4s	-50%
`keccakf1600_extract_bytes (big endian)`	✅	2s	3s	-33%
`keccakf1600_xor_bytes`	✅	2s	1s	+100%
`keccakf1600x4_permute`	✅	2s	2s	+0%
`keccakf1600x4_xor_bytes`	✅	2s	1s	+100%
`keccakf1600x4_xor_bytes_native`	✅	2s	2s	+0%
`make_hint`	✅	2s	2s	+0%
`mld_ct_abs_i32`	✅	2s	1s	+100%
`mld_ct_cmask_nonzero_u8`	✅	2s	2s	+0%
`mld_ct_memcmp`	✅	2s	1s	+100%
`mld_h`	✅	2s	2s	+0%
`mld_keccakf1600_extract_bytes`	✅	2s	1s	+100%
`mld_prepare_domain_separation_prefix`	✅	2s	3s	-33%
`ntt_native_aarch64`	✅	2s	4s	-50%
`nttunpack_native_x86_64`	✅	2s	3s	-33%
`pack_sig_c`	✅	2s	2s	+0%
`pack_sk_s1`	✅	2s	2s	+0%
`pointwise_native_aarch64`	✅	2s	4s	-50%
`pointwise_native_x86_64`	✅	2s	5s	-60%
`poly_caddq`	✅	2s	5s	-60%
`poly_challenge`	✅	2s	4s	-50%
`poly_decompose`	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	✅	2s	3s	-33%
`poly_decompose_88_native_aarch64`	✅	2s	2s	+0%
`poly_decompose_c`	✅	2s	6s	-67%
`poly_decompose_native_x86_64`	✅	2s	3s	-33%
`poly_invntt_tomont`	✅	2s	4s	-50%
`poly_permute_bitrev_to_custom_optional`	✅	2s	2s	+0%
`poly_pointwise_montgomery`	✅	2s	3s	-33%
`poly_pointwise_montgomery_native`	✅	2s	3s	-33%
`poly_reduce`	✅	2s	4s	-50%
`poly_sub`	✅	2s	5s	-60%
`poly_uniform`	✅	2s	4s	-50%
`poly_uniform_4x`	✅	2s	3s	-33%
`poly_uniform_eta`	✅	2s	5s	-60%
`poly_use_hint_native_aarch64`	✅	2s	3s	-33%
`polyveck_caddq`	✅	2s	8s	-75%
`polyveck_pack_w1`	✅	2s	3s	-33%
`polyveck_unpack_eta`	✅	2s	3s	-33%
`polyvecl_uniform_gamma1_serial`	✅	2s	2s	+0%
`polyvecl_unpack_z`	✅	2s	3s	-33%
`polyw1_pack`	✅	2s	2s	+0%
`polyw1_pack_88`	✅	2s	2s	+0%
`polyz_unpack`	✅	2s	3s	-33%
`polyz_unpack_c`	✅	2s	7s	-71%
`polyz_unpack_native`	✅	2s	1s	+100%
`reduce32`	✅	2s	3s	-33%
`rej_uniform_eta_native_x86_64`	✅	2s	-	new
`rej_uniform_native`	✅	2s	5s	-60%
`rej_uniform_native_aarch64`	✅	2s	3s	-33%
`shake256_absorb`	✅	2s	3s	-33%
`shake256_squeeze`	✅	2s	2s	+0%
`shake256x4_squeezeblocks`	✅	2s	4s	-50%
`sign_verify_extmu`	✅	2s	4s	-50%
`sign_verify_pre_hash_internal`	✅	2s	3s	-33%
`sign_verify_pre_hash_shake256`	✅	2s	7s	-71%
`sk_s2hat_get_poly`	✅	2s	2s	+0%
`unpack_sk_s1hat`	✅	2s	3s	-33%
`yvec_init`	✅	2s	4s	-50%
`fqscale`	✅	1s	1s	+0%
`keccak_f1600_x1_native_aarch64`	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	1s	2s	-50%
`keccak_f1600_x4_native_avx2`	✅	1s	3s	-67%
`keccakf1600_permute_native`	✅	1s	3s	-67%
`mld_ct_cmask_neg_i32`	✅	1s	2s	-50%
`mld_ct_get_optblocker_u8`	✅	1s	3s	-67%
`mld_keccakf1600x4_xor_bytes_c`	✅	1s	1s	+0%
`mld_polymat_expand_entry`	✅	1s	4s	-75%
`mld_value_barrier_i64`	✅	1s	2s	-50%
`mld_value_barrier_u8`	✅	1s	2s	-50%
`pack_sig_z`	✅	1s	3s	-67%
`poly_caddq_c`	✅	1s	3s	-67%
`poly_caddq_native`	✅	1s	3s	-67%
`poly_decompose_native`	✅	1s	2s	-50%
`poly_shiftl`	✅	1s	4s	-75%
`poly_uniform_gamma1_4x`	✅	1s	3s	-67%
`poly_use_hint`	✅	1s	4s	-75%
`poly_use_hint_c`	✅	1s	4s	-75%
`poly_use_hint_native_x86_64`	✅	1s	-	new
`polyvec_matrix_expand`	✅	1s	3s	-67%
`polyveck_chknorm`	✅	1s	9s	-89%
`polyvecl_pointwise_acc_montgomery_c`	✅	1s	2s	-50%
`polyvecl_pointwise_acc_montgomery_native`	✅	1s	2s	-50%
`polyz_unpack_17_native_aarch64`	✅	1s	4s	-75%
`rej_eta_c`	✅	1s	4s	-75%
`shake128_finalize`	✅	1s	2s	-50%
`shake128_init`	✅	1s	2s	-50%
`shake128x4_absorb_once`	✅	1s	4s	-75%
`shake256`	✅	1s	3s	-67%
`shake256_finalize`	✅	1s	3s	-67%
`shake256_init`	✅	1s	3s	-67%
`shake256_release`	✅	1s	5s	-80%
`shake256x4_absorb_once`	✅	1s	5s	-80%
`sign_verify`	✅	1s	2s	-50%
`sys_check_capability`	✅	1s	2s	-50%
`unpack_pk_t1`	✅	1s	2s	-50%
`use_hint`	✅	1s	3s	-67%

oqs-bot · 2026-07-10T16:10:53Z

CBMC Results (ML-DSA-65)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`compute_pack_t0_t1`	⚠️	122s	13s	+838%
`mld_attempt_signature_generation`	⚠️	235s	63s	+273%
`sig_unpack_hints`	⚠️	26s	2s	+1200%
`sign_keypair_internal`	⚠️	20s	5s	+300%
`sign_pk_from_sk`	⚠️	38s	6s	+533%
`sign_signature_internal`	⚠️	178s	55s	+224%
`sign_verify_internal`	⚠️	363s	177s	+105%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	2042s	1784s	+14.5%
`sign_verify_internal`	⚠️	363s	177s	+105%
`mld_attempt_signature_generation`	⚠️	235s	63s	+273%
`sign_signature_internal`	⚠️	178s	55s	+224%
`polyvecl_pointwise_acc_montgomery_c`	✅	159s	210s	-24%
`poly_pointwise_montgomery_c`	✅	132s	125s	+6%
`compute_pack_t0_t1`	⚠️	122s	13s	+838%
`polyvec_matrix_expand`	✅	71s	110s	-35%
`mld_invntt_layer`	✅	56s	109s	-49%
`sign_pk_from_sk`	⚠️	38s	6s	+533%
`sig_unpack_hints`	⚠️	26s	2s	+1200%
`fqmul`	✅	22s	40s	-45%
`mld_ntt_layer`	✅	20s	41s	-51%
`sign_keypair_internal`	⚠️	20s	5s	+300%
`polyvec_matrix_expand_serial`	✅	17s	27s	-37%
`polyveck_ntt`	✅	15s	7s	+114%
`keccakf1600x4_permute_native`	✅	14s	23s	-39%
`mld_ntt_butterfly_block`	✅	11s	24s	-54%
`poly_ntt_c`	✅	10s	19s	-47%
`polyveck_decompose`	✅	10s	12s	-17%
`polyt0_unpack`	✅	8s	16s	-50%
`rej_uniform`	✅	8s	18s	-56%
`rej_uniform_native_x86_64`	✅	8s	-	new
`poly_invntt_tomont_c`	✅	7s	11s	-36%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	7s	18s	-61%
`keccak_absorb`	✅	6s	3s	+100%
`keccak_absorb_once_x4`	✅	6s	8s	-25%
`mld_check_pct`	✅	6s	14s	-57%
`poly_chknorm_c`	✅	6s	15s	-60%
`poly_uniform_eta_4x`	✅	6s	14s	-57%
`polyveck_caddq`	✅	6s	6s	+0%
`rej_uniform_c`	✅	6s	14s	-57%
`intt_native_x86_64`	✅	5s	3s	+67%
`keccak_squeezeblocks_x4`	✅	5s	5s	+0%
`mld_compute_pack_z`	✅	5s	7s	-29%
`poly_add`	✅	5s	9s	-44%
`poly_uniform_4x`	✅	5s	13s	-62%
`polyt1_unpack`	✅	5s	5s	+0%
`polyveck_pack_w1`	✅	5s	3s	+67%
`polyvecl_ntt`	✅	5s	4s	+25%
`keccakf1600_xor_bytes`	✅	4s	2s	+100%
`keccakf1600_xor_bytes (big endian)`	✅	4s	2s	+100%
`mld_polymat_expand_entry`	✅	4s	4s	+0%
`ntt_native_x86_64`	✅	4s	2s	+100%
`nttunpack_native_x86_64`	✅	4s	3s	+33%
`pointwise_acc_native_aarch64`	✅	4s	6s	-33%
`pointwise_acc_native_x86_64`	✅	4s	8s	-50%
`poly_permute_bitrev_to_custom_optional_native`	✅	4s	4s	+0%
`poly_shiftl`	✅	4s	3s	+33%
`poly_uniform_gamma1`	✅	4s	3s	+33%
`poly_use_hint_native`	✅	4s	2s	+100%
`polyveck_chknorm`	✅	4s	6s	-33%
`polyveck_invntt_tomont`	✅	4s	8s	-50%
`rej_uniform_native`	✅	4s	4s	+0%
`rej_uniform_native_aarch64`	✅	4s	3s	+33%
`shake256_squeeze`	✅	4s	3s	+33%
`sign_keypair`	✅	4s	3s	+33%
`sign_signature_pre_hash_shake256`	✅	4s	3s	+33%
`sign_verify_pre_hash_internal`	✅	4s	5s	-20%
`sign_verify_pre_hash_shake256`	✅	4s	5s	-20%
`unpack_sk_s1hat`	✅	4s	2s	+100%
`unpack_sk_s2hat`	✅	4s	4s	+0%
`yvec_get_poly`	✅	4s	3s	+33%
`decompose`	✅	3s	1s	+200%
`intt_native_aarch64`	✅	3s	3s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	✅	3s	4s	-25%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	3s	2s	+50%
`keccak_f1600_x4_native_avx2`	✅	3s	2s	+50%
`keccak_squeeze`	✅	3s	4s	-25%
`keccakf1600x4_extract_bytes`	✅	3s	4s	-25%
`keccakf1600x4_xor_bytes`	✅	3s	1s	+200%
`mld_ct_abs_i32`	✅	3s	2s	+50%
`mld_ct_cmask_neg_i32`	✅	3s	2s	+50%
`mld_ct_get_optblocker_i64`	✅	3s	2s	+50%
`mld_h`	✅	3s	2s	+50%
`mld_keccakf1600_extract_bytes`	✅	3s	1s	+200%
`mld_keccakf1600_permute_c`	✅	3s	6s	-50%
`mld_keccakf1600x4_xor_bytes_c`	✅	3s	2s	+50%
`mld_prepare_domain_separation_prefix`	✅	3s	2s	+50%
`mld_sign_attempt`	✅	3s	-	new
`mld_sign_finish`	✅	3s	-	new
`ntt_native_aarch64`	✅	3s	2s	+50%
`pack_sig_c`	✅	3s	5s	-40%
`pack_sig_z`	✅	3s	2s	+50%
`pointwise_native_aarch64`	✅	3s	5s	-40%
`poly_caddq_native`	✅	3s	2s	+50%
`poly_caddq_native_x86_64`	✅	3s	3s	+0%
`poly_chknorm`	✅	3s	4s	-25%
`poly_decompose_c`	✅	3s	5s	-40%
`poly_power2round`	✅	3s	4s	-25%
`poly_use_hint_c`	✅	3s	5s	-40%
`poly_use_hint_native_aarch64`	✅	3s	3s	+0%
`poly_use_hint_native_x86_64`	✅	3s	-	new
`polyeta_unpack`	✅	3s	8s	-62%
`polyvecl_chknorm`	✅	3s	7s	-57%
`polyvecl_unpack_z`	✅	3s	3s	+0%
`polyw1_pack_88`	✅	3s	2s	+50%
`polyz_unpack_17_native_aarch64`	✅	3s	3s	+0%
`polyz_unpack_c`	✅	3s	13s	-77%
`power2round`	✅	3s	1s	+200%
`rej_eta_c`	✅	3s	5s	-40%
`shake128_finalize`	✅	3s	1s	+200%
`shake256_absorb`	✅	3s	2s	+50%
`shake256_release`	✅	3s	2s	+50%
`sign_signature_extmu`	✅	3s	2s	+50%
`sign_signature_pre_hash_internal`	✅	3s	3s	+0%
`sk_s1hat_get_poly`	✅	3s	6s	-50%
`sk_s2hat_get_poly`	✅	3s	2s	+50%
`sk_t0hat_get_poly`	✅	3s	2s	+50%
`unpack_sk`	✅	3s	3s	+0%
`use_hint`	✅	3s	2s	+50%
`caddq`	✅	2s	3s	-33%
`fqscale`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	3s	-33%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	2s	+0%
`keccak_init`	✅	2s	1s	+100%
`keccakf1600_permute`	✅	2s	2s	+0%
`keccakf1600_permute_native`	✅	2s	3s	-33%
`keccakf1600x4_extract_bytes_native`	✅	2s	4s	-50%
`make_hint`	✅	2s	2s	+0%
`mld_ct_cmask_nonzero_u32`	✅	2s	4s	-50%
`mld_ct_cmask_nonzero_u8`	✅	2s	3s	-33%
`mld_ct_get_optblocker_u32`	✅	2s	3s	-33%
`mld_ct_get_optblocker_u8`	✅	2s	2s	+0%
`mld_ct_memcmp`	✅	2s	2s	+0%
`mld_ct_sel_int32`	✅	2s	3s	-33%
`mld_keccakf1600x4_extract_bytes_c`	✅	2s	3s	-33%
`mld_sample_s1_s2`	✅	2s	6s	-67%
`mld_sample_s1_s2_serial`	✅	2s	4s	-50%
`mld_sign_resume`	✅	2s	-	new
`montgomery_reduce`	✅	2s	4s	-50%
`pack_sk_s1`	✅	2s	5s	-60%
`pointwise_native_x86_64`	✅	2s	3s	-33%
`poly_caddq`	✅	2s	2s	+0%
`poly_caddq_c`	✅	2s	2s	+0%
`poly_challenge`	✅	2s	6s	-67%
`poly_decompose`	✅	2s	2s	+0%
`poly_decompose_88_native_aarch64`	✅	2s	1s	+100%
`poly_decompose_native`	✅	2s	3s	-33%
`poly_decompose_native_x86_64`	✅	2s	3s	-33%
`poly_invntt_tomont_native`	✅	2s	2s	+0%
`poly_ntt`	✅	2s	2s	+0%
`poly_permute_bitrev_to_custom_optional`	✅	2s	2s	+0%
`poly_pointwise_montgomery_native`	✅	2s	3s	-33%
`poly_reduce`	✅	2s	3s	-33%
`poly_sub`	✅	2s	3s	-33%
`poly_uniform`	✅	2s	4s	-50%
`poly_uniform_eta`	✅	2s	4s	-50%
`poly_uniform_gamma1_4x`	✅	2s	4s	-50%
`poly_use_hint`	✅	2s	3s	-33%
`polyeta_pack`	✅	2s	3s	-33%
`polyt0_pack`	✅	2s	3s	-33%
`polyt1_pack`	✅	2s	3s	-33%
`polyvec_matrix_pointwise_montgomery_row`	✅	2s	1s	+100%
`polyveck_pack_eta`	✅	2s	4s	-50%
`polyveck_unpack_eta`	✅	2s	6s	-67%
`polyvecl_pack_eta`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	2s	+0%
`polyvecl_uniform_gamma1`	✅	2s	2s	+0%
`polyvecl_unpack_eta`	✅	2s	3s	-33%
`polyw1_pack_32`	✅	2s	4s	-50%
`polyz_pack`	✅	2s	3s	-33%
`polyz_unpack_native`	✅	2s	4s	-50%
`rej_eta`	✅	2s	2s	+0%
`rej_uniform_eta_native_aarch64`	✅	2s	4s	-50%
`rej_uniform_eta_native_x86_64`	✅	2s	-	new
`shake128_init`	✅	2s	2s	+0%
`shake128_release`	✅	2s	3s	-33%
`shake128x4_absorb_once`	✅	2s	3s	-33%
`shake128x4_squeezeblocks`	✅	2s	3s	-33%
`shake256`	✅	2s	2s	+0%
`shake256_init`	✅	2s	2s	+0%
`sign_signature`	✅	2s	6s	-67%
`sign_verify`	✅	2s	3s	-33%
`sign_verify_extmu`	✅	2s	3s	-33%
`unpack_sk_t0hat`	✅	2s	5s	-60%
`yvec_init`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64`	✅	1s	2s	-50%
`keccak_finalize`	✅	1s	2s	-50%
`keccakf1600_extract_bytes (big endian)`	✅	1s	2s	-50%
`keccakf1600x4_permute`	✅	1s	4s	-75%
`keccakf1600x4_xor_bytes_native`	✅	1s	3s	-67%
`mld_value_barrier_i64`	✅	1s	2s	-50%
`mld_value_barrier_u32`	✅	1s	3s	-67%
`mld_value_barrier_u8`	✅	1s	3s	-67%
`pack_sig_h`	✅	1s	5s	-80%
`pack_sk_rho_key_tr_s2`	✅	1s	2s	-50%
`poly_caddq_native_aarch64`	✅	1s	2s	-50%
`poly_chknorm_native`	✅	1s	2s	-50%
`poly_chknorm_native_aarch64`	✅	1s	3s	-67%
`poly_chknorm_native_x86_64`	✅	1s	3s	-67%
`poly_decompose_32_native_aarch64`	✅	1s	3s	-67%
`poly_invntt_tomont`	✅	1s	3s	-67%
`poly_ntt_native`	✅	1s	4s	-75%
`poly_pointwise_montgomery`	✅	1s	3s	-67%
`polyveck_reduce`	✅	1s	4s	-75%
`polyvecl_uniform_gamma1_serial`	✅	1s	3s	-67%
`polyw1_pack`	✅	1s	4s	-75%
`polyz_unpack`	✅	1s	3s	-67%
`polyz_unpack_19_native_aarch64`	✅	1s	3s	-67%
`polyz_unpack_native_x86_64`	✅	1s	3s	-67%
`reduce32`	✅	1s	3s	-67%
`rej_eta_native`	✅	1s	3s	-67%
`shake128_absorb`	✅	1s	2s	-50%
`shake128_squeeze`	✅	1s	2s	-50%
`shake256_finalize`	✅	1s	1s	+0%
`shake256x4_absorb_once`	✅	1s	3s	-67%
`shake256x4_squeezeblocks`	✅	1s	2s	-50%
`sys_check_capability`	✅	1s	4s	-75%
`unpack_pk_t1`	✅	1s	5s	-80%

oqs-bot · 2026-07-10T16:11:02Z

CBMC Results (ML-DSA-65, REDUCE-RAM)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`compute_pack_t0_t1`	⚠️	34s	7s	+386%
`mld_attempt_signature_generation`	⚠️	140s	31s	+352%
`sign_keypair_internal`	⚠️	27s	3s	+800%
`sign_pk_from_sk`	⚠️	51s	5s	+920%
`sign_verify_internal`	⚠️	156s	71s	+120%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	✅	1284s	1482s	-13.4%
`sign_verify_internal`	⚠️	156s	71s	+120%
`mld_attempt_signature_generation`	⚠️	140s	31s	+352%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	136s	201s	-32%
`poly_pointwise_montgomery_c`	✅	62s	116s	-47%
`mld_invntt_layer`	✅	56s	108s	-48%
`sign_pk_from_sk`	⚠️	51s	5s	+920%
`polyvecl_chknorm`	✅	47s	43s	+9%
`compute_pack_t0_t1`	⚠️	34s	7s	+386%
`sign_keypair_internal`	⚠️	27s	3s	+800%
`fqmul`	✅	23s	40s	-43%
`mld_ntt_layer`	✅	23s	43s	-47%
`keccakf1600x4_permute_native`	✅	12s	22s	-45%
`sign_signature_internal`	✅	12s	6s	+100%
`poly_uniform_eta_4x`	✅	10s	13s	-23%
`sig_unpack_hints`	✅	10s	1s	+900%
`mld_ntt_butterfly_block`	✅	9s	25s	-64%
`poly_ntt_c`	✅	9s	22s	-59%
`polyt0_unpack`	✅	9s	13s	-31%
`rej_uniform_c`	✅	9s	16s	-44%
`rej_uniform`	✅	8s	7s	+14%
`rej_uniform_native_x86_64`	✅	8s	-	new
`poly_invntt_tomont_c`	✅	7s	10s	-30%
`keccak_absorb_once_x4`	✅	6s	10s	-40%
`polyveck_caddq`	✅	6s	7s	-14%
`mld_ct_cmask_nonzero_u8`	✅	5s	2s	+150%
`pointwise_acc_native_x86_64`	✅	5s	5s	+0%
`pointwise_native_x86_64`	✅	5s	2s	+150%
`polyveck_decompose`	✅	5s	14s	-64%
`sign_signature_pre_hash_shake256`	✅	5s	7s	-29%
`sign_verify`	✅	5s	6s	-17%
`mld_check_pct`	✅	4s	12s	-67%
`mld_ct_get_optblocker_u32`	✅	4s	3s	+33%
`pointwise_acc_native_aarch64`	✅	4s	6s	-33%
`poly_challenge`	✅	4s	5s	-20%
`poly_chknorm_c`	✅	4s	13s	-69%
`poly_ntt`	✅	4s	2s	+100%
`poly_pointwise_montgomery_native`	✅	4s	4s	+0%
`poly_uniform_gamma1`	✅	4s	3s	+33%
`poly_use_hint_native`	✅	4s	7s	-43%
`polyeta_unpack`	✅	4s	4s	+0%
`polyvec_matrix_pointwise_montgomery_row`	✅	4s	8s	-50%
`polyveck_invntt_tomont`	✅	4s	7s	-43%
`polyvecl_pack_eta`	✅	4s	2s	+100%
`polyvecl_uniform_gamma1`	✅	4s	4s	+0%
`shake256`	✅	4s	2s	+100%
`keccak_squeezeblocks_x4`	✅	3s	4s	-25%
`keccakf1600_extract_bytes (big endian)`	✅	3s	3s	+0%
`keccakf1600x4_extract_bytes`	✅	3s	4s	-25%
`keccakf1600x4_permute`	✅	3s	1s	+200%
`make_hint`	✅	3s	3s	+0%
`mld_keccakf1600_extract_bytes`	✅	3s	2s	+50%
`mld_prepare_domain_separation_prefix`	✅	3s	4s	-25%
`mld_sample_s1_s2`	✅	3s	6s	-50%
`mld_sample_s1_s2_serial`	✅	3s	3s	+0%
`mld_sign_finish`	✅	3s	-	new
`mld_sign_resume`	✅	3s	-	new
`ntt_native_aarch64`	✅	3s	3s	+0%
`pointwise_native_aarch64`	✅	3s	3s	+0%
`poly_add`	✅	3s	7s	-57%
`poly_caddq`	✅	3s	3s	+0%
`poly_decompose_native`	✅	3s	5s	-40%
`poly_invntt_tomont_native`	✅	3s	5s	-40%
`poly_permute_bitrev_to_custom_optional_native`	✅	3s	3s	+0%
`poly_reduce`	✅	3s	4s	-25%
`poly_use_hint`	✅	3s	3s	+0%
`polyt1_pack`	✅	3s	3s	+0%
`polyt1_unpack`	✅	3s	3s	+0%
`polyvec_matrix_expand_serial`	✅	3s	3s	+0%
`polyvecl_ntt`	✅	3s	7s	-57%
`polyvecl_unpack_eta`	✅	3s	2s	+50%
`polyw1_pack`	✅	3s	3s	+0%
`polyz_pack`	✅	3s	3s	+0%
`polyz_unpack`	✅	3s	3s	+0%
`polyz_unpack_17_native_aarch64`	✅	3s	2s	+50%
`polyz_unpack_c`	✅	3s	9s	-67%
`rej_eta_native`	✅	3s	3s	+0%
`rej_uniform_native`	✅	3s	4s	-25%
`shake128_finalize`	✅	3s	2s	+50%
`shake128x4_squeezeblocks`	✅	3s	2s	+50%
`shake256_init`	✅	3s	4s	-25%
`sign_keypair`	✅	3s	4s	-25%
`sign_signature`	✅	3s	5s	-40%
`sign_verify_extmu`	✅	3s	2s	+50%
`sign_verify_pre_hash_internal`	✅	3s	5s	-40%
`sign_verify_pre_hash_shake256`	✅	3s	6s	-50%
`sk_s2hat_get_poly`	✅	3s	1s	+200%
`yvec_get_poly`	✅	3s	3s	+0%
`caddq`	✅	2s	2s	+0%
`decompose`	✅	2s	4s	-50%
`fqscale`	✅	2s	3s	-33%
`intt_native_aarch64`	✅	2s	2s	+0%
`intt_native_x86_64`	✅	2s	4s	-50%
`keccak_absorb`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v84a`	✅	2s	2s	+0%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	2s	3s	-33%
`keccakf1600_permute`	✅	2s	4s	-50%
`keccakf1600_permute_native`	✅	2s	2s	+0%
`keccakf1600_xor_bytes`	✅	2s	4s	-50%
`keccakf1600x4_extract_bytes_native`	✅	2s	1s	+100%
`keccakf1600x4_xor_bytes_native`	✅	2s	2s	+0%
`mld_compute_pack_z`	✅	2s	5s	-60%
`mld_ct_cmask_nonzero_u32`	✅	2s	3s	-33%
`mld_ct_get_optblocker_i64`	✅	2s	1s	+100%
`mld_ct_memcmp`	✅	2s	4s	-50%
`mld_h`	✅	2s	3s	-33%
`mld_keccakf1600_permute_c`	✅	2s	7s	-71%
`mld_polymat_expand_entry`	✅	2s	3s	-33%
`mld_value_barrier_u8`	✅	2s	1s	+100%
`montgomery_reduce`	✅	2s	1s	+100%
`nttunpack_native_x86_64`	✅	2s	3s	-33%
`pack_sig_c`	✅	2s	3s	-33%
`pack_sk_rho_key_tr_s2`	✅	2s	2s	+0%
`poly_caddq_native`	✅	2s	4s	-50%
`poly_caddq_native_aarch64`	✅	2s	2s	+0%
`poly_caddq_native_x86_64`	✅	2s	1s	+100%
`poly_chknorm`	✅	2s	3s	-33%
`poly_chknorm_native_aarch64`	✅	2s	2s	+0%
`poly_chknorm_native_x86_64`	✅	2s	4s	-50%
`poly_decompose`	✅	2s	2s	+0%
`poly_decompose_32_native_aarch64`	✅	2s	4s	-50%
`poly_decompose_c`	✅	2s	8s	-75%
`poly_invntt_tomont`	✅	2s	5s	-60%
`poly_permute_bitrev_to_custom_optional`	✅	2s	3s	-33%
`poly_power2round`	✅	2s	7s	-71%
`poly_shiftl`	✅	2s	3s	-33%
`poly_sub`	✅	2s	4s	-50%
`poly_uniform`	✅	2s	2s	+0%
`poly_uniform_gamma1_4x`	✅	2s	3s	-33%
`poly_use_hint_c`	✅	2s	2s	+0%
`polyt0_pack`	✅	2s	5s	-60%
`polyvec_matrix_expand`	✅	2s	6s	-67%
`polyveck_chknorm`	✅	2s	36s	-94%
`polyveck_ntt`	✅	2s	4s	-50%
`polyveck_pack_eta`	✅	2s	3s	-33%
`polyveck_pack_w1`	✅	2s	4s	-50%
`polyveck_reduce`	✅	2s	6s	-67%
`polyvecl_pointwise_acc_montgomery`	✅	2s	3s	-33%
`polyvecl_pointwise_acc_montgomery_native`	✅	2s	3s	-33%
`polyvecl_uniform_gamma1_serial`	✅	2s	1s	+100%
`polyvecl_unpack_z`	✅	2s	1s	+100%
`polyw1_pack_88`	✅	2s	3s	-33%
`polyz_unpack_native_x86_64`	✅	2s	3s	-33%
`reduce32`	✅	2s	2s	+0%
`rej_eta`	✅	2s	5s	-60%
`rej_eta_c`	✅	2s	4s	-50%
`rej_uniform_eta_native_aarch64`	✅	2s	5s	-60%
`rej_uniform_eta_native_x86_64`	✅	2s	-	new
`rej_uniform_native_aarch64`	✅	2s	5s	-60%
`shake128_init`	✅	2s	6s	-67%
`shake128_release`	✅	2s	2s	+0%
`shake256_finalize`	✅	2s	1s	+100%
`shake256_release`	✅	2s	3s	-33%
`sign_signature_extmu`	✅	2s	4s	-50%
`sign_signature_pre_hash_internal`	✅	2s	3s	-33%
`sk_t0hat_get_poly`	✅	2s	1s	+100%
`sys_check_capability`	✅	2s	1s	+100%
`unpack_sk_s1hat`	✅	2s	1s	+100%
`unpack_sk_s2hat`	✅	2s	3s	-33%
`unpack_sk_t0hat`	✅	2s	4s	-50%
`use_hint`	✅	2s	2s	+0%
`yvec_init`	✅	2s	5s	-60%
`keccak_f1600_x1_native_aarch64_v84a`	✅	1s	2s	-50%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	1s	3s	-67%
`keccak_f1600_x4_native_avx2`	✅	1s	2s	-50%
`keccak_finalize`	✅	1s	2s	-50%
`keccak_init`	✅	1s	4s	-75%
`keccak_squeeze`	✅	1s	2s	-50%
`keccakf1600_xor_bytes (big endian)`	✅	1s	2s	-50%
`keccakf1600x4_xor_bytes`	✅	1s	2s	-50%
`mld_ct_abs_i32`	✅	1s	6s	-83%
`mld_ct_cmask_neg_i32`	✅	1s	3s	-67%
`mld_ct_get_optblocker_u8`	✅	1s	4s	-75%
`mld_ct_sel_int32`	✅	1s	2s	-50%
`mld_keccakf1600x4_extract_bytes_c`	✅	1s	2s	-50%
`mld_keccakf1600x4_xor_bytes_c`	✅	1s	2s	-50%
`mld_sign_attempt`	✅	1s	-	new
`mld_value_barrier_i64`	✅	1s	2s	-50%
`mld_value_barrier_u32`	✅	1s	4s	-75%
`ntt_native_x86_64`	✅	1s	5s	-80%
`pack_sig_h`	✅	1s	2s	-50%
`pack_sig_z`	✅	1s	1s	+0%
`pack_sk_s1`	✅	1s	3s	-67%
`poly_caddq_c`	✅	1s	5s	-80%
`poly_chknorm_native`	✅	1s	4s	-75%
`poly_decompose_88_native_aarch64`	✅	1s	2s	-50%
`poly_decompose_native_x86_64`	✅	1s	2s	-50%
`poly_ntt_native`	✅	1s	2s	-50%
`poly_pointwise_montgomery`	✅	1s	2s	-50%
`poly_uniform_4x`	✅	1s	4s	-75%
`poly_uniform_eta`	✅	1s	5s	-80%
`poly_use_hint_native_aarch64`	✅	1s	4s	-75%
`poly_use_hint_native_x86_64`	✅	1s	-	new
`polyeta_pack`	✅	1s	1s	+0%
`polyveck_unpack_eta`	✅	1s	3s	-67%
`polyvecl_pointwise_acc_montgomery_c`	✅	1s	3s	-67%
`polyw1_pack_32`	✅	1s	2s	-50%
`polyz_unpack_19_native_aarch64`	✅	1s	5s	-80%
`polyz_unpack_native`	✅	1s	3s	-67%
`power2round`	✅	1s	2s	-50%
`shake128_absorb`	✅	1s	2s	-50%
`shake128_squeeze`	✅	1s	3s	-67%
`shake128x4_absorb_once`	✅	1s	2s	-50%
`shake256_absorb`	✅	1s	4s	-75%
`shake256_squeeze`	✅	1s	4s	-75%
`shake256x4_absorb_once`	✅	1s	2s	-50%
`shake256x4_squeezeblocks`	✅	1s	2s	-50%
`sk_s1hat_get_poly`	✅	1s	3s	-67%
`unpack_pk_t1`	✅	1s	2s	-50%
`unpack_sk`	✅	1s	3s	-67%

oqs-bot · 2026-07-10T16:14:08Z

CBMC Results (ML-DSA-87)

⚠️ Attention Required

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	2974s	2151s	+38.3%
`compute_pack_t0_t1`	⚠️	200s	19s	+953%
`mld_attempt_signature_generation`	⚠️	310s	55s	+464%
`sig_unpack_hints`	⚠️	30s	3s	+900%
`sign_keypair_internal`	⚠️	56s	6s	+833%
`sign_pk_from_sk`	⚠️	52s	6s	+767%
`sign_signature_internal`	⚠️	342s	42s	+714%
`sign_verify_internal`	⚠️	786s	97s	+710%

Full Results (210 proofs)

Proof	Status	Current	Previous	Change
`TOTAL`	⚠️	2974s	2151s	+38.3%
`sign_verify_internal`	⚠️	786s	97s	+710%
`sign_signature_internal`	⚠️	342s	42s	+714%
`mld_attempt_signature_generation`	⚠️	310s	55s	+464%
`polyvecl_pointwise_acc_montgomery_c`	✅	246s	353s	-30%
`compute_pack_t0_t1`	⚠️	200s	19s	+953%
`poly_pointwise_montgomery_c`	✅	150s	144s	+4%
`polyvec_matrix_expand`	✅	89s	324s	-73%
`mld_invntt_layer`	✅	63s	115s	-45%
`sign_keypair_internal`	⚠️	56s	6s	+833%
`sign_pk_from_sk`	⚠️	52s	6s	+767%
`sig_unpack_hints`	⚠️	30s	3s	+900%
`mld_ntt_layer`	✅	25s	45s	-44%
`polyvec_matrix_expand_serial`	✅	25s	38s	-34%
`fqmul`	✅	23s	43s	-47%
`keccakf1600x4_permute_native`	✅	13s	23s	-43%
`mld_ntt_butterfly_block`	✅	12s	24s	-50%
`polyvec_matrix_pointwise_montgomery_yvec`	✅	12s	18s	-33%
`polyt0_unpack`	✅	11s	14s	-21%
`rej_uniform`	✅	10s	15s	-33%
`rej_uniform_native_x86_64`	✅	10s	-	new
`mld_check_pct`	✅	9s	16s	-44%
`poly_ntt_c`	✅	9s	21s	-57%
`poly_chknorm_c`	✅	8s	15s	-47%
`polyeta_unpack`	✅	8s	17s	-53%
`rej_uniform_c`	✅	8s	19s	-58%
`poly_uniform_eta_4x`	✅	7s	11s	-36%
`keccak_absorb_once_x4`	✅	6s	9s	-33%
`mld_compute_pack_z`	✅	6s	8s	-25%
`poly_invntt_tomont_c`	✅	6s	12s	-50%
`poly_power2round`	✅	6s	3s	+100%
`polyveck_caddq`	✅	6s	8s	-25%
`polyveck_decompose`	✅	6s	13s	-54%
`sign_signature_pre_hash_shake256`	✅	6s	6s	+0%
`mld_sign_resume`	✅	5s	-	new
`poly_caddq_c`	✅	5s	3s	+67%
`poly_decompose_native_x86_64`	✅	5s	2s	+150%
`poly_uniform_4x`	✅	5s	13s	-62%
`polyveck_invntt_tomont`	✅	5s	9s	-44%
`polyveck_ntt`	✅	5s	11s	-55%
`polyvecl_chknorm`	✅	5s	7s	-29%
`polyz_unpack_c`	✅	5s	3s	+67%
`rej_eta_c`	✅	5s	5s	+0%
`sign_keypair`	✅	5s	4s	+25%
`sign_signature_extmu`	✅	5s	4s	+25%
`sign_verify_pre_hash_shake256`	✅	5s	3s	+67%
`keccak_absorb`	✅	4s	3s	+33%
`mld_prepare_domain_separation_prefix`	✅	4s	4s	+0%
`mld_sample_s1_s2`	✅	4s	6s	-33%
`pointwise_acc_native_x86_64`	✅	4s	6s	-33%
`poly_caddq_native_x86_64`	✅	4s	2s	+100%
`poly_permute_bitrev_to_custom_optional_native`	✅	4s	5s	-20%
`poly_use_hint_native_x86_64`	✅	4s	-	new
`polyveck_pack_w1`	✅	4s	3s	+33%
`polyvecl_ntt`	✅	4s	7s	-43%
`polyvecl_pack_eta`	✅	4s	3s	+33%
`polyvecl_pointwise_acc_montgomery_native`	✅	4s	3s	+33%
`polyw1_pack_32`	✅	4s	4s	+0%
`shake256`	✅	4s	2s	+100%
`sign_verify_pre_hash_internal`	✅	4s	3s	+33%
`keccak_f1600_x1_native_aarch64`	✅	3s	1s	+200%
`keccak_f1600_x4_native_aarch64_v84a`	✅	3s	4s	-25%
`keccak_squeezeblocks_x4`	✅	3s	4s	-25%
`keccakf1600_extract_bytes (big endian)`	✅	3s	3s	+0%
`keccakf1600_permute`	✅	3s	3s	+0%
`mld_ct_get_optblocker_u8`	✅	3s	3s	+0%
`mld_keccakf1600_permute_c`	✅	3s	7s	-57%
`mld_sample_s1_s2_serial`	✅	3s	8s	-62%
`mld_sign_finish`	✅	3s	-	new
`montgomery_reduce`	✅	3s	3s	+0%
`pointwise_acc_native_aarch64`	✅	3s	6s	-50%
`pointwise_native_aarch64`	✅	3s	5s	-40%
`poly_decompose_c`	✅	3s	5s	-40%
`poly_decompose_native`	✅	3s	2s	+50%
`poly_pointwise_montgomery_native`	✅	3s	5s	-40%
`poly_sub`	✅	3s	3s	+0%
`poly_uniform`	✅	3s	4s	-25%
`poly_use_hint_native`	✅	3s	3s	+0%
`polyvec_matrix_pointwise_montgomery_row`	✅	3s	3s	+0%
`polyveck_chknorm`	✅	3s	3s	+0%
`polyveck_pack_eta`	✅	3s	6s	-50%
`polyvecl_uniform_gamma1`	✅	3s	2s	+50%
`polyw1_pack_88`	✅	3s	3s	+0%
`polyz_pack`	✅	3s	5s	-40%
`polyz_unpack`	✅	3s	2s	+50%
`polyz_unpack_native`	✅	3s	4s	-25%
`polyz_unpack_native_x86_64`	✅	3s	3s	+0%
`rej_eta`	✅	3s	4s	-25%
`rej_uniform_native`	✅	3s	8s	-62%
`shake128_finalize`	✅	3s	2s	+50%
`shake256_init`	✅	3s	2s	+50%
`shake256x4_absorb_once`	✅	3s	2s	+50%
`sign_signature_pre_hash_internal`	✅	3s	5s	-40%
`sign_verify`	✅	3s	5s	-40%
`unpack_sk`	✅	3s	5s	-40%
`yvec_init`	✅	3s	4s	-25%
`decompose`	✅	2s	3s	-33%
`intt_native_aarch64`	✅	2s	3s	-33%
`intt_native_x86_64`	✅	2s	3s	-33%
`keccak_f1600_x1_native_aarch64_v84a`	✅	2s	1s	+100%
`keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid`	✅	2s	3s	-33%
`keccak_init`	✅	2s	3s	-33%
`keccak_squeeze`	✅	2s	2s	+0%
`keccakf1600_permute_native`	✅	2s	4s	-50%
`keccakf1600x4_extract_bytes_native`	✅	2s	2s	+0%
`make_hint`	✅	2s	3s	-33%
`mld_ct_abs_i32`	✅	2s	3s	-33%
`mld_ct_cmask_neg_i32`	✅	2s	4s	-50%
`mld_ct_cmask_nonzero_u32`	✅	2s	2s	+0%
`mld_ct_get_optblocker_i64`	✅	2s	3s	-33%
`mld_ct_sel_int32`	✅	2s	3s	-33%
`mld_h`	✅	2s	3s	-33%
`mld_keccakf1600_extract_bytes`	✅	2s	4s	-50%
`mld_keccakf1600x4_extract_bytes_c`	✅	2s	2s	+0%
`mld_sign_attempt`	✅	2s	-	new
`mld_value_barrier_u8`	✅	2s	3s	-33%
`ntt_native_aarch64`	✅	2s	6s	-67%
`ntt_native_x86_64`	✅	2s	2s	+0%
`nttunpack_native_x86_64`	✅	2s	3s	-33%
`pack_sig_h`	✅	2s	4s	-50%
`pack_sig_z`	✅	2s	5s	-60%
`pack_sk_rho_key_tr_s2`	✅	2s	3s	-33%
`pack_sk_s1`	✅	2s	1s	+100%
`pointwise_native_x86_64`	✅	2s	2s	+0%
`poly_add`	✅	2s	6s	-67%
`poly_caddq`	✅	2s	2s	+0%
`poly_caddq_native`	✅	2s	4s	-50%
`poly_caddq_native_aarch64`	✅	2s	3s	-33%
`poly_challenge`	✅	2s	5s	-60%
`poly_chknorm`	✅	2s	3s	-33%
`poly_chknorm_native_x86_64`	✅	2s	2s	+0%
`poly_decompose`	✅	2s	3s	-33%
`poly_decompose_32_native_aarch64`	✅	2s	5s	-60%
`poly_decompose_88_native_aarch64`	✅	2s	2s	+0%
`poly_invntt_tomont`	✅	2s	1s	+100%
`poly_ntt`	✅	2s	3s	-33%
`poly_ntt_native`	✅	2s	3s	-33%
`poly_permute_bitrev_to_custom_optional`	✅	2s	3s	-33%
`poly_reduce`	✅	2s	2s	+0%
`poly_shiftl`	✅	2s	4s	-50%
`poly_uniform_gamma1`	✅	2s	4s	-50%
`poly_uniform_gamma1_4x`	✅	2s	3s	-33%
`poly_use_hint`	✅	2s	1s	+100%
`poly_use_hint_c`	✅	2s	2s	+0%
`poly_use_hint_native_aarch64`	✅	2s	2s	+0%
`polyeta_pack`	✅	2s	4s	-50%
`polyt1_pack`	✅	2s	3s	-33%
`polyt1_unpack`	✅	2s	4s	-50%
`polyveck_reduce`	✅	2s	3s	-33%
`polyveck_unpack_eta`	✅	2s	4s	-50%
`polyvecl_pointwise_acc_montgomery`	✅	2s	5s	-60%
`polyvecl_uniform_gamma1_serial`	✅	2s	4s	-50%
`polyvecl_unpack_eta`	✅	2s	5s	-60%
`polyz_unpack_17_native_aarch64`	✅	2s	3s	-33%
`power2round`	✅	2s	4s	-50%
`reduce32`	✅	2s	3s	-33%
`rej_eta_native`	✅	2s	6s	-67%
`rej_uniform_eta_native_aarch64`	✅	2s	5s	-60%
`rej_uniform_eta_native_x86_64`	✅	2s	-	new
`rej_uniform_native_aarch64`	✅	2s	2s	+0%
`shake128_absorb`	✅	2s	4s	-50%
`shake128_init`	✅	2s	1s	+100%
`shake128_squeeze`	✅	2s	2s	+0%
`shake256_absorb`	✅	2s	2s	+0%
`shake256_finalize`	✅	2s	2s	+0%
`shake256_release`	✅	2s	3s	-33%
`shake256x4_squeezeblocks`	✅	2s	1s	+100%
`sign_verify_extmu`	✅	2s	3s	-33%
`sk_s1hat_get_poly`	✅	2s	3s	-33%
`sk_s2hat_get_poly`	✅	2s	3s	-33%
`unpack_sk_s1hat`	✅	2s	2s	+0%
`unpack_sk_s2hat`	✅	2s	3s	-33%
`unpack_sk_t0hat`	✅	2s	7s	-71%
`use_hint`	✅	2s	3s	-33%
`yvec_get_poly`	✅	2s	4s	-50%
`caddq`	✅	1s	4s	-75%
`fqscale`	✅	1s	3s	-67%
`keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid`	✅	1s	4s	-75%
`keccak_f1600_x4_native_avx2`	✅	1s	2s	-50%
`keccak_finalize`	✅	1s	1s	+0%
`keccakf1600_xor_bytes`	✅	1s	3s	-67%
`keccakf1600_xor_bytes (big endian)`	✅	1s	2s	-50%
`keccakf1600x4_extract_bytes`	✅	1s	2s	-50%
`keccakf1600x4_permute`	✅	1s	3s	-67%
`keccakf1600x4_xor_bytes`	✅	1s	3s	-67%
`keccakf1600x4_xor_bytes_native`	✅	1s	3s	-67%
`mld_ct_cmask_nonzero_u8`	✅	1s	3s	-67%
`mld_ct_get_optblocker_u32`	✅	1s	2s	-50%
`mld_ct_memcmp`	✅	1s	3s	-67%
`mld_keccakf1600x4_xor_bytes_c`	✅	1s	4s	-75%
`mld_polymat_expand_entry`	✅	1s	3s	-67%
`mld_value_barrier_i64`	✅	1s	1s	+0%
`mld_value_barrier_u32`	✅	1s	2s	-50%
`pack_sig_c`	✅	1s	4s	-75%
`poly_chknorm_native`	✅	1s	4s	-75%
`poly_chknorm_native_aarch64`	✅	1s	4s	-75%
`poly_invntt_tomont_native`	✅	1s	5s	-80%
`poly_pointwise_montgomery`	✅	1s	4s	-75%
`poly_uniform_eta`	✅	1s	4s	-75%
`polyt0_pack`	✅	1s	4s	-75%
`polyvecl_unpack_z`	✅	1s	4s	-75%
`polyw1_pack`	✅	1s	4s	-75%
`polyz_unpack_19_native_aarch64`	✅	1s	4s	-75%
`shake128_release`	✅	1s	4s	-75%
`shake128x4_absorb_once`	✅	1s	5s	-80%
`shake128x4_squeezeblocks`	✅	1s	3s	-67%
`shake256_squeeze`	✅	1s	2s	-50%
`sign_signature`	✅	1s	5s	-80%
`sk_t0hat_get_poly`	✅	1s	4s	-75%
`sys_check_capability`	✅	1s	3s	-67%
`unpack_pk_t1`	✅	1s	1s	+0%

bremoran · 2026-07-28T16:00:58Z

Depends on either #1312 or #1318

Build the ABI checker and assembly sources directly with Zephyr's target toolchain. Select the Armv8.1-M checker for M55 and preserve OPT/AUTO through the run stage so the checker is actually executed. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Include OPT, the selected FIPS202 backend, and configurable test counts in the active build marker so changes to those inputs rebuild stale Zephyr binaries. Track the native assembly amalgamation and its direct development-source include as explicit dependencies, and allow QEMU execution timeouts to be overridden. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Signed-off-by: Brendan Moran <brendan.moran@arm.com>

The lazy/eager polyvector unit test allocates both ML-DSA-87 representations and their scratch space through MLD_ALLOC. The default MLD_ALLOC implementation expands to aligned automatic arrays, so this single test exceeds the Zephyr test thread stack on the Cortex-M55 test configuration. Use test-local, aligned static buffers for this workspace. The TEST_STATIC_ALLOC and TEST_STATIC_FREE helpers are deliberately scoped to test_unit.c: they preserve cleanup by zeroizing every buffer and clearing its pointer, without changing the allocator used by production code or other tests. Only test/src/test_unit.c changes. The test inputs, comparisons, and coverage remain the same; this commit changes where its temporary workspace is stored. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Generated ABI checks normally fill every assembly argument buffer with random bytes. That is unsuitable for interfaces containing control data. The Armv8.1-M Keccak x1 permutation consumes 49 round-constant words and requires the final word to be 0x000000ff as a loop terminator. Leaving that word random can make the checker read beyond the supplied buffer. Add an optional test_bytes mapping to buffer entries in the assembly ABI YAML. scripts/autogen validates that offsets are integers within the buffer and that values are bytes, sorts the overrides, and emits them after randombytes initializes the rest of the buffer. Existing ABI metadata without test_bytes retains its current behaviour. Document the new metadata in test/abicheck/README.md. The generic facility is introduced here before its Keccak x1 consumer so the following backend commit contains only feature-specific metadata and generated checks. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Add the first of three deliberately separated Cortex-M55 Keccak changes: a known-good scalar baseline derived from the Adomnicai/XKCP Armv7-M implementation. Measurements made while preparing the series showed that the existing Cortex-M7 schedule runs faster on Cortex-M55 than the Cortex-M4 schedule, so this commit establishes the M7-scheduled implementation before later commits introduce an M55 scheduling model and a 64-bit load/store-aware scalar input. The code in this commit is scalar and does not require or use MVE. Keep the Keccak state in the even/odd bit-interleaved representation across permutations. Native xor and extract hooks convert only the lanes crossing the byte interface, and a private round-constant table supplies the 24 interleaved constants and loop terminator expected by the permutation. Organize the implementation so its origin and generated form remain reviewable. dev/fips202/armv81m_clean contains only the unscheduled permutation input. dev/fips202/armv81m_opt contains the SLOTHY driver, Makefile, concise development README, C wrapper, scheduled permutation, and separate scalar xor and extract assembly sources. Splitting the helpers gives every assembly file one external entry point and lets the normal loop-label check cover all x1 sources. Teach scripts/autogen to merge the existing Armv8.1-M and new x1 development directories into the production directory. The retained filename set is derived from both inputs, replacing the hard-coded keep list and ensuring removed or renamed files cannot leave stale output. The helper assembly is simplified and synchronized like other production assembly, so mldsa_native_asm.S includes only files under mldsa/ and no longer reaches into dev/. Zephyr custom builds track all production assembly inputs for reliable rebuilds. Describe and generate AAPCS32 checks for all three external assembly routines: permutation, xor, and extract. The scalar routines carry no MVE feature requirement. Add focused xor and extract tests for zero length, unaligned starts, 7/8/9-byte lane boundaries, cross-lane ranges, final-lane ranges, and the complete 200-byte state; canary-filled extraction buffers also detect writes beyond the requested length. Existing representation-aware permutation tests continue to compare against the portable reference. Update the bibliography and license material for the imported XKCP, Adomnicai, and SLOTHY work. Keep the x1 header, constants, sources, generation path, tests, and ABI metadata separate from the established parallel implementation so no x4 source file is changed. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

oqs-bot

Graviton4 (no-opt)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`127897` cycles	`127841` cycles	`1.00`
`ML-DSA-44 sign`	`441495` cycles	`440929` cycles	`1.00`
`ML-DSA-44 verify`	`136358` cycles	`136340` cycles	`1.00`
`ML-DSA-65 keypair`	`221663` cycles	`221539` cycles	`1.00`
`ML-DSA-65 sign`	`714078` cycles	`713985` cycles	`1.00`
`ML-DSA-65 verify`	`220580` cycles	`220544` cycles	`1.00`
`ML-DSA-87 keypair`	`365287` cycles	`364498` cycles	`1.00`
`ML-DSA-87 sign`	`916065` cycles	`915431` cycles	`1.00`
`ML-DSA-87 verify`	`370911` cycles	`371022` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton3 (no-opt)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`138441` cycles	`138205` cycles	`1.00`
`ML-DSA-44 sign`	`486106` cycles	`485764` cycles	`1.00`
`ML-DSA-44 verify`	`149269` cycles	`149259` cycles	`1.00`
`ML-DSA-65 keypair`	`242153` cycles	`241613` cycles	`1.00`
`ML-DSA-65 sign`	`791700` cycles	`791618` cycles	`1.00`
`ML-DSA-65 verify`	`241534` cycles	`241503` cycles	`1.00`
`ML-DSA-87 keypair`	`396162` cycles	`395195` cycles	`1.00`
`ML-DSA-87 sign`	`1013608` cycles	`1014135` cycles	`1.00`
`ML-DSA-87 verify`	`403785` cycles	`404031` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Intel Xeon 4th gen (c7i)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`43290` cycles	`43407` cycles	`1.00`
`ML-DSA-44 sign`	`130107` cycles	`130440` cycles	`1.00`
`ML-DSA-44 verify`	`45233` cycles	`45231` cycles	`1.00`
`ML-DSA-65 keypair`	`75800` cycles	`75611` cycles	`1.00`
`ML-DSA-65 sign`	`213743` cycles	`213750` cycles	`1.00`
`ML-DSA-65 verify`	`74411` cycles	`74462` cycles	`1.00`
`ML-DSA-87 keypair`	`122926` cycles	`122917` cycles	`1.00`
`ML-DSA-87 sign`	`270981` cycles	`271210` cycles	`1.00`
`ML-DSA-87 verify`	`120778` cycles	`120613` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

AMD EPYC 4th gen (c7a)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`46735` cycles	`46709` cycles	`1.00`
`ML-DSA-44 sign`	`139947` cycles	`139435` cycles	`1.00`
`ML-DSA-44 verify`	`49469` cycles	`49461` cycles	`1.00`
`ML-DSA-65 keypair`	`82621` cycles	`81967` cycles	`1.01`
`ML-DSA-65 sign`	`227154` cycles	`226735` cycles	`1.00`
`ML-DSA-65 verify`	`81978` cycles	`82665` cycles	`0.99`
`ML-DSA-87 keypair`	`130551` cycles	`129492` cycles	`1.01`
`ML-DSA-87 sign`	`279924` cycles	`280340` cycles	`1.00`
`ML-DSA-87 verify`	`128506` cycles	`128405` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Intel Xeon 4th gen (c7i) (no-opt)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`91704` cycles	`91774` cycles	`1.00`
`ML-DSA-44 sign`	`351502` cycles	`351709` cycles	`1.00`
`ML-DSA-44 verify`	`99387` cycles	`99709` cycles	`1.00`
`ML-DSA-65 keypair`	`154237` cycles	`154289` cycles	`1.00`
`ML-DSA-65 sign`	`571927` cycles	`570738` cycles	`1.00`
`ML-DSA-65 verify`	`160351` cycles	`160181` cycles	`1.00`
`ML-DSA-87 keypair`	`255233` cycles	`255166` cycles	`1.00`
`ML-DSA-87 sign`	`720046` cycles	`720821` cycles	`1.00`
`ML-DSA-87 verify`	`264335` cycles	`263865` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton2

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`112198` cycles	`112399` cycles	`1.00`
`ML-DSA-44 sign`	`353753` cycles	`353820` cycles	`1.00`
`ML-DSA-44 verify`	`117415` cycles	`117171` cycles	`1.00`
`ML-DSA-65 keypair`	`194605` cycles	`194786` cycles	`1.00`
`ML-DSA-65 sign`	`584072` cycles	`584013` cycles	`1.00`
`ML-DSA-65 verify`	`193382` cycles	`193015` cycles	`1.00`
`ML-DSA-87 keypair`	`320883` cycles	`320852` cycles	`1.00`
`ML-DSA-87 sign`	`747307` cycles	`747201` cycles	`1.00`
`ML-DSA-87 verify`	`318179` cycles	`318645` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

AMD EPYC 3rd gen (c6a)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`52008` cycles	`51879` cycles	`1.00`
`ML-DSA-44 sign`	`154462` cycles	`155064` cycles	`1.00`
`ML-DSA-44 verify`	`54166` cycles	`54259` cycles	`1.00`
`ML-DSA-65 keypair`	`89427` cycles	`89685` cycles	`1.00`
`ML-DSA-65 sign`	`253071` cycles	`254754` cycles	`0.99`
`ML-DSA-65 verify`	`89176` cycles	`89439` cycles	`1.00`
`ML-DSA-87 keypair`	`143367` cycles	`142352` cycles	`1.01`
`ML-DSA-87 sign`	`310438` cycles	`311341` cycles	`1.00`
`ML-DSA-87 verify`	`138807` cycles	`139359` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

AMD EPYC 4th gen (c7a) (no-opt)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`118639` cycles	`118234` cycles	`1.00`
`ML-DSA-44 sign`	`458559` cycles	`458712` cycles	`1.00`
`ML-DSA-44 verify`	`130837` cycles	`131121` cycles	`1.00`
`ML-DSA-65 keypair`	`201470` cycles	`200822` cycles	`1.00`
`ML-DSA-65 sign`	`743521` cycles	`747583` cycles	`0.99`
`ML-DSA-65 verify`	`209873` cycles	`209481` cycles	`1.00`
`ML-DSA-87 keypair`	`331170` cycles	`332858` cycles	`0.99`
`ML-DSA-87 sign`	`935608` cycles	`936652` cycles	`1.00`
`ML-DSA-87 verify`	`343114` cycles	`343994` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

AMD EPYC 3rd gen (c6a) (no-opt)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`133187` cycles	`134282` cycles	`0.99`
`ML-DSA-44 sign`	`518022` cycles	`520818` cycles	`0.99`
`ML-DSA-44 verify`	`146634` cycles	`147777` cycles	`0.99`
`ML-DSA-65 keypair`	`224332` cycles	`224694` cycles	`1.00`
`ML-DSA-65 sign`	`843960` cycles	`843127` cycles	`1.00`
`ML-DSA-65 verify`	`234144` cycles	`233924` cycles	`1.00`
`ML-DSA-87 keypair`	`367057` cycles	`367125` cycles	`1.00`
`ML-DSA-87 sign`	`1058600` cycles	`1057892` cycles	`1.00`
`ML-DSA-87 verify`	`380447` cycles	`380252` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton2 (no-opt)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`212129` cycles	`212335` cycles	`1.00`
`ML-DSA-44 sign`	`760693` cycles	`761210` cycles	`1.00`
`ML-DSA-44 verify`	`229484` cycles	`229974` cycles	`1.00`
`ML-DSA-65 keypair`	`375440` cycles	`376324` cycles	`1.00`
`ML-DSA-65 sign`	`1248106` cycles	`1248564` cycles	`1.00`
`ML-DSA-65 verify`	`371579` cycles	`372377` cycles	`1.00`
`ML-DSA-87 keypair`	`600041` cycles	`601386` cycles	`1.00`
`ML-DSA-87 sign`	`1586041` cycles	`1607791` cycles	`0.99`
`ML-DSA-87 verify`	`615917` cycles	`617602` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Intel Xeon 3rd gen (c6i)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`61706` cycles	`61819` cycles	`1.00`
`ML-DSA-44 sign`	`187966` cycles	`188851` cycles	`1.00`
`ML-DSA-44 verify`	`66228` cycles	`66399` cycles	`1.00`
`ML-DSA-65 keypair`	`109427` cycles	`110427` cycles	`0.99`
`ML-DSA-65 sign`	`311800` cycles	`313769` cycles	`0.99`
`ML-DSA-65 verify`	`109443` cycles	`111323` cycles	`0.98`
`ML-DSA-87 keypair`	`170673` cycles	`173116` cycles	`0.99`
`ML-DSA-87 sign`	`379405` cycles	`385429` cycles	`0.98`
`ML-DSA-87 verify`	`170627` cycles	`174422` cycles	`0.98`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Intel Xeon 3rd gen (c6i) (no-opt)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`154055` cycles	`154452` cycles	`1.00`
`ML-DSA-44 sign`	`587101` cycles	`588162` cycles	`1.00`
`ML-DSA-44 verify`	`169059` cycles	`168998` cycles	`1.00`
`ML-DSA-65 keypair`	`261730` cycles	`262562` cycles	`1.00`
`ML-DSA-65 sign`	`964081` cycles	`965903` cycles	`1.00`
`ML-DSA-65 verify`	`271336` cycles	`272372` cycles	`1.00`
`ML-DSA-87 keypair`	`431609` cycles	`431929` cycles	`1.00`
`ML-DSA-87 sign`	`1212961` cycles	`1211899` cycles	`1.00`
`ML-DSA-87 verify`	`447991` cycles	`447459` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Arm Cortex-M55 (NUCLEO-N657X0-Q) benchmarks (opt)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`1690331` cycles	`2328440` cycles	`0.73`
`ML-DSA-44 sign`	`13600033` cycles	`17851737` cycles	`0.76`
`ML-DSA-44 verify`	`1806518` cycles	`2398876` cycles	`0.75`
`ML-DSA-65 keypair`	`2895358` cycles	`4025122` cycles	`0.72`
`ML-DSA-65 sign`	`11228232` cycles	`14793522` cycles	`0.76`
`ML-DSA-65 verify`	`2973684` cycles	`4012792` cycles	`0.74`
`ML-DSA-87 keypair`	`4888795` cycles	`6864887` cycles	`0.71`
`ML-DSA-87 sign`	`18455928` cycles	`24785157` cycles	`0.74`
`ML-DSA-87 verify`	`5009804` cycles	`6864412` cycles	`0.73`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Arm Cortex-M55 (NUCLEO-N657X0-Q) benchmarks (no-opt)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`2328440` cycles	`2328440` cycles	`1`
`ML-DSA-44 sign`	`17851737` cycles	`17851737` cycles	`1`
`ML-DSA-44 verify`	`2398876` cycles	`2398876` cycles	`1`
`ML-DSA-65 keypair`	`4025122` cycles	`4025122` cycles	`1`
`ML-DSA-65 sign`	`14793522` cycles	`14793522` cycles	`1`
`ML-DSA-65 verify`	`4012792` cycles	`4012792` cycles	`1`
`ML-DSA-87 keypair`	`6864887` cycles	`6864887` cycles	`1`
`ML-DSA-87 sign`	`24785157` cycles	`24785157` cycles	`1`
`ML-DSA-87 verify`	`6864412` cycles	`6864412` cycles	`1`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Arm Cortex-A55 (Snapdragon 888) benchmarks (opt)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`272258` cycles	`271067` cycles	`1.00`
`ML-DSA-44 sign`	`811182` cycles	`812320` cycles	`1.00`
`ML-DSA-44 verify`	`273722` cycles	`273045` cycles	`1.00`
`ML-DSA-65 keypair`	`467921` cycles	`467726` cycles	`1.00`
`ML-DSA-65 sign`	`1374610` cycles	`1341160` cycles	`1.02`
`ML-DSA-65 verify`	`452328` cycles	`454368` cycles	`1.00`
`ML-DSA-87 keypair`	`794593` cycles	`803830` cycles	`0.99`
`ML-DSA-87 sign`	`1852551` cycles	`1831323` cycles	`1.01`
`ML-DSA-87 verify`	`781142` cycles	`778295` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Arm Cortex-A55 (Snapdragon 888) benchmarks (no-opt)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`465428` cycles	`465494` cycles	`1.00`
`ML-DSA-44 sign`	`2134682` cycles	`2144256` cycles	`1.00`
`ML-DSA-44 verify`	`556859` cycles	`559936` cycles	`0.99`
`ML-DSA-65 keypair`	`784546` cycles	`783372` cycles	`1.00`
`ML-DSA-65 sign`	`3502813` cycles	`3496274` cycles	`1.00`
`ML-DSA-65 verify`	`867806` cycles	`869188` cycles	`1.00`
`ML-DSA-87 keypair`	`1265637` cycles	`1266792` cycles	`1.00`
`ML-DSA-87 sign`	`4348278` cycles	`4317269` cycles	`1.01`
`ML-DSA-87 verify`	`1387880` cycles	`1394437` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (opt)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`218060` cycles	`216344` cycles	`1.01`
`ML-DSA-44 sign`	`597336` cycles	`593807` cycles	`1.01`
`ML-DSA-44 verify`	`217728` cycles	`216553` cycles	`1.01`
`ML-DSA-65 keypair`	`380946` cycles	`378995` cycles	`1.01`
`ML-DSA-65 sign`	`983605` cycles	`982529` cycles	`1.00`
`ML-DSA-65 verify`	`363319` cycles	`363919` cycles	`1.00`
`ML-DSA-87 keypair`	`636094` cycles	`636641` cycles	`1.00`
`ML-DSA-87 sign`	`1312206` cycles	`1318452` cycles	`1.00`
`ML-DSA-87 verify`	`617779` cycles	`619777` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

Arm Cortex-A72 (Raspberry Pi 4) benchmarks (no-opt)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`301299` cycles	`301210` cycles	`1.00`
`ML-DSA-44 sign`	`1140771` cycles	`1141652` cycles	`1.00`
`ML-DSA-44 verify`	`333412` cycles	`330898` cycles	`1.01`
`ML-DSA-65 keypair`	`550692` cycles	`543839` cycles	`1.01`
`ML-DSA-65 sign`	`1876845` cycles	`1856990` cycles	`1.01`
`ML-DSA-65 verify`	`533547` cycles	`525059` cycles	`1.02`
`ML-DSA-87 keypair`	`845041` cycles	`846962` cycles	`1.00`
`ML-DSA-87 sign`	`2351108` cycles	`2362668` cycles	`1.00`
`ML-DSA-87 verify`	`874370` cycles	`876584` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

github-actions

SpacemiT K1 8 (Banana Pi F3) benchmarks (no-opt)

Details

Benchmark suite	Current: `91039f7`	Previous: `27aebe7`	Ratio
`ML-DSA-44 keypair`	`760366` cycles	`760367` cycles	`1.00`
`ML-DSA-44 sign`	`3142358` cycles	`3140398` cycles	`1.00`
`ML-DSA-44 verify`	`859639` cycles	`859497` cycles	`1.00`
`ML-DSA-65 keypair`	`1287922` cycles	`1289584` cycles	`1.00`
`ML-DSA-65 sign`	`5081104` cycles	`5091406` cycles	`1.00`
`ML-DSA-65 verify`	`1367411` cycles	`1368454` cycles	`1.00`
`ML-DSA-87 keypair`	`2109891` cycles	`2109786` cycles	`1.00`
`ML-DSA-87 sign`	`6360762` cycles	`6373090` cycles	`1.00`
`ML-DSA-87 verify`	`2224537` cycles	`2226888` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

Make the clean M7 Keccak source self-contained so SLOTHY retains its ABI metadata and integration guards during regeneration. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

bremoran · 2026-08-05T08:59:15Z

Added metadata YAML to the input source file so that slothy will preserve it and autogen will pass. This is a comment-only change and benchmarks do not need to be re-run.

mkannwischer

Thanks @bremoran.

I have a number of comments. Please look at the LICENSE first as that will likely block this PR.

mkannwischer · 2026-08-10T08:39:50Z

+#if defined(MLD_USE_NATIVE_FIPS202_X1_EXTRACT_BYTES)
+  if (mld_keccakf1600_extract_bytes_x1_native(state, data, offset, length) ==
+      MLD_NATIVE_FUNC_SUCCESS)
+  {
+    return;
+  }
+#endif /* MLD_USE_NATIVE_FIPS202_X1_EXTRACT_BYTES */
 #if defined(MLD_SYS_LITTLE_ENDIAN)
  uint8_t *state_ptr = (uint8_t *)state + offset;


This breaks C90 on platforms impkementing exract bytes due to the state_ptr declaration a little lower. that needs to be fixed. Also maybe worth switching to C90 to catch this in the future (unless this leads to more problems, then please open an issue).

mkannwischer · 2026-08-12T04:25:12Z

+/* The Adomnicai x1 core consumes 24 bit-interleaved round constants followed
+ * by a 0xff loop terminator. Keep this table private to this backend. */
+static MLD_ALIGN const uint32_t mld_keccakf1600_round_constants_x1[49] = {
+    0x00000001, 0x00000000, /* RC0 */
+    0x00000000, 0x00000089, /* RC1 */
+    0x00000000, 0x8000008b, /* RC2 */
+    0x00000000, 0x80008080, /* RC3 */
+    0x00000001, 0x0000008b, /* RC4 */
+    0x00000001, 0x00008000, /* RC5 */
+    0x00000001, 0x80008088, /* RC6 */
+    0x00000001, 0x80000082, /* RC7 */
+    0x00000000, 0x0000000b, /* RC8 */
+    0x00000000, 0x0000000a, /* RC9 */
+    0x00000001, 0x00008082, /* RC10 */
+    0x00000000, 0x00008003, /* RC11 */
+    0x00000001, 0x0000808b, /* RC12 */
+    0x00000001, 0x8000000b, /* RC13 */
+    0x00000001, 0x8000008a, /* RC14 */
+    0x00000001, 0x80000081, /* RC15 */
+    0x00000000, 0x80000081, /* RC16 */
+    0x00000000, 0x80000008, /* RC17 */
+    0x00000000, 0x00000083, /* RC18 */
+    0x00000000, 0x80008003, /* RC19 */
+    0x00000001, 0x80008088, /* RC20 */
+    0x00000000, 0x80000088, /* RC21 */
+    0x00000001, 0x00008000, /* RC22 */
+    0x00000000, 0x80008082, /* RC23 */
+    0x000000ff,             /* loop terminator */
+};


Please auto generate in autogen this in a similar way it is autogenerated for other platforms.

mkannwischer · 2026-08-12T04:26:17Z

+                                                 unsigned offset,
+                                                 unsigned length);
+
+/* The Adomnicai x1 core consumes 24 bit-interleaved round constants followed


Let's acknowledge the source of this implementation once in the assembly and then keep all other comments general, i.e., do not talk about the Adomnicai x1 core - it only leads to confusion later on.

mkannwischer · 2026-08-12T04:27:53Z

+ */
+
+/*
+ * This helper is derived from the public-domain XKCP implementation and the


Be more specific here: CC0. public domain means different things for different people.

mkannwischer · 2026-08-12T04:32:46Z

+
+/*
+ * This helper is derived from the public-domain XKCP implementation and the
+ * Armv7-M optimizations described in [ADOMNICAI23]. See the backend README,


Please cite the implementation directly

mkannwischer · 2026-08-12T05:18:08Z

-ZEPHYR_FIPS202_BACKEND_mps3-an547 := fips202/native/armv81m/mve.h
-ZEPHYR_FIPS202_BACKEND_nucleo-n657x0-q := fips202/native/armv81m/mve.h
+ZEPHYR_FIPS202_BACKEND_mps3-an547 := fips202/native/armv81m/mve_x1.h
+ZEPHYR_FIPS202_BACKEND_nucleo-n657x0-q := fips202/native/armv81m/mve_x1.h


This swaps out the backend. Does this introduce a test gap as the x4 Keccak is no longer tested? We should not be regressing test coverage, so we need to at least add a x4 unit test to CI.

mkannwischer · 2026-08-12T05:19:15Z

+
+#define mld_keccak_f1600_x1_native_impl \
+  MLD_NAMESPACE(keccak_f1600_x1_native_impl)
+int mld_keccak_f1600_x1_native_impl(uint64_t *state);


These should be marked MLD_INTERNAL_API

mkannwischer · 2026-08-12T05:21:17Z

+QEMU_TIMEOUT ?= 300
+export QEMU_TIMEOUT
+
 # Native backends are an OPT=1 feature (an547 builds the Armv8.1-M MVE backend).


mkannwischer · 2026-08-12T05:25:06Z

@@ -65,48 +65,75 @@ unsigned int mld_rej_eta_c(int32_t *a, unsigned int target, unsigned int offset,
 void mld_keccakf1600_permute_c(uint64_t *state);

 #if defined(MLD_USE_NATIVE_FIPS202_X1)


CI does not run unit tests for Armv8.1-M. Please enable it.

mkannwischer · 2026-08-12T05:30:44Z

+The Armv8.1-M Keccak implementation contains portions adapted from SLOTHY
+examples distributed under the MIT license. The applicable SLOTHY copyright
+notices are included below.
+


Which portions are MIT licensed? I did not see any file in this PR being MIT-only licensed and we wouldn't be able to take it for anything under mldsa/. Maybe this is an outdated notice that can be removed?

Move the x1 constants into armv81m_opt and add a triple-licensed SLOTHY driver targeting Cortex-M7. Preserve x4 implementation sources and retain their CI coverage with a focused unit test. Document CC0 provenance, regenerate the production sources, and remove the obsolete MIT-only scheduler and license notice. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Signed-off-by: Brendan Moran <brendan.moran@arm.com>

bremoran requested a review from a team as a code owner July 10, 2026 08:11

mkannwischer marked this pull request as draft July 10, 2026 08:18

bremoran force-pushed the armv81m-keccak-x1 branch 3 times, most recently from a1dde44 to e8a49a1 Compare July 14, 2026 10:42

bremoran force-pushed the armv81m-keccak-x1 branch from d0543bf to c45a108 Compare July 23, 2026 11:03

bremoran mentioned this pull request Jul 24, 2026

CI: Disable ABI checks on Zephyr targets #1312

Closed

bremoran force-pushed the armv81m-keccak-x1 branch 2 times, most recently from 4f71edb to 1c70ab2 Compare August 3, 2026 12:46

bremoran added 3 commits August 3, 2026 17:16

Test: Preserve build mode when running tests

c4a6ece

Signed-off-by: Brendan Moran <brendan.moran@arm.com>

bremoran force-pushed the armv81m-keccak-x1 branch from 1c70ab2 to 3ed4031 Compare August 3, 2026 17:03

bremoran added 3 commits August 4, 2026 07:32

bremoran force-pushed the armv81m-keccak-x1 branch from 14b78cc to 91039f7 Compare August 4, 2026 13:56

bremoran added the benchmark label Aug 4, 2026

oqs-bot reviewed Aug 4, 2026

View reviewed changes

github-actions Bot reviewed Aug 4, 2026

View reviewed changes

bremoran mentioned this pull request Aug 4, 2026

Test: Run ABI checks as Zephyr applications #1318

Merged

github-actions Bot reviewed Aug 4, 2026

View reviewed changes

Armv8.1-M: preserve Keccak metadata through SLOTHY

962c9f9

Make the clean M7 Keccak source self-contained so SLOTHY retains its ABI metadata and integration guards during regeneration. Signed-off-by: Brendan Moran <brendan.moran@arm.com>

bremoran mentioned this pull request Aug 5, 2026

Armv8.1-M: regenerate Keccak x1 for Cortex-M55 #1356

Open

bremoran marked this pull request as ready for review August 6, 2026 08:14

bremoran requested review from hanno-becker and mkannwischer August 7, 2026 07:22

mkannwischer requested changes Aug 12, 2026

View reviewed changes

bremoran added 3 commits August 20, 2026 09:53

Merge branch 'main' into armv81m-keccak-x1

af2a114

Signed-off-by: Brendan Moran <brendan.moran@arm.com>

Autogen: Fix Ruff formatting

ade6b34

Signed-off-by: Brendan Moran <brendan.moran@arm.com>

		@@ -65,48 +65,75 @@ unsigned int mld_rej_eta_c(int32_t *a, unsigned int target, unsigned int offset,
		void mld_keccakf1600_permute_c(uint64_t *state);

		#if defined(MLD_USE_NATIVE_FIPS202_X1)

Uh oh!

Conversation

bremoran commented Jul 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

oqs-bot commented Jul 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-44)

Uh oh!

oqs-bot commented Jul 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-44, REDUCE-RAM)

Uh oh!

oqs-bot commented Jul 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-87, REDUCE-RAM)

Uh oh!

oqs-bot commented Jul 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-65)

Uh oh!

oqs-bot commented Jul 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-65, REDUCE-RAM)

Uh oh!

oqs-bot commented Jul 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CBMC Results (ML-DSA-87)

Uh oh!

bremoran commented Jul 28, 2026

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton4 (no-opt)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton3 (no-opt)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Intel Xeon 4th gen (c7i)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

AMD EPYC 4th gen (c7a)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Intel Xeon 4th gen (c7i) (no-opt)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton2

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

AMD EPYC 3rd gen (c6a)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

AMD EPYC 4th gen (c7a) (no-opt)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

AMD EPYC 3rd gen (c6a) (no-opt)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton2 (no-opt)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Intel Xeon 3rd gen (c6i)

Uh oh!

oqs-bot left a comment

Choose a reason for hiding this comment

Intel Xeon 3rd gen (c6i) (no-opt)

Uh oh!

github-actions Bot left a comment

bremoran commented Jul 10, 2026 •

edited

Loading

oqs-bot commented Jul 10, 2026 •

edited

Loading

oqs-bot commented Jul 10, 2026 •

edited

Loading

oqs-bot commented Jul 10, 2026 •

edited

Loading

oqs-bot commented Jul 10, 2026 •

edited

Loading

oqs-bot commented Jul 10, 2026 •

edited

Loading

oqs-bot commented Jul 10, 2026 •

edited

Loading

bremoran commented Aug 5, 2026 •

edited

Loading